index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
cc
/
cctac.ml4
Age
Commit message (
Expand
)
Author
2005-08-17
new congruence
corbinea
2005-02-18
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-12
Uniformisation de destApplication en destApp
herbelin
2005-02-06
Nettoyage et documentation de Library
herbelin
2005-01-14
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2004-07-16
Nouvelle en-tête
herbelin
2004-03-14
minor changes
corbinea
2004-03-14
congruence now handles disequalities
corbinea
2004-02-06
correction de bugs de congruence et firstorder (inductifs)
corbinea
2004-01-09
bugs avec Pose et Assert
barras
2003-12-09
cc update
corbinea
2003-12-02
error messages adjustement
corbinea
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
2003-11-20
Code simplification in CC
corbinea
2003-03-31
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2002-11-14
Réforme de l'interprétation des termes :
herbelin
2002-10-01
Adding the congruence closure tactics (CC and CCsolve).
corbinea
