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