index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
cc.v
Commit message (
Expand
)
Author
Age
*
Congruence: Fixing a bug with native projections.
Hugo Herbelin
2018-03-27
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
*
congruence: Restrict refreshing to Set
Matthieu Sozeau
2016-07-04
*
|
Using build_selector from Equality as a replacement of the selector
Hugo Herbelin
2016-03-05
|
/
*
fix bug #2447 in congruence
Pierre Corbineau
2014-12-16
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
congruence now knows about _ -> _
corbinea
2008-02-21
*
Correction du bug #1679 (congruence) et ajout test-suite
corbinea
2007-09-14
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...
herbelin
2005-09-09
*
ground->firstorder, cc-> congruence, CC final commit
corbinea
2003-11-29
*
removal of CC.v lemata in cc (deprecated)
corbinea
2003-11-26
*
CC: added injection theory
corbinea
2003-11-25
*
Adding the congruence closure tactics (CC and CCsolve).
corbinea
2002-10-01