aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/cc/cctac.ml4
Commit message (Expand)AuthorAge
* correction de bugs de congruence et firstorder (inductifs)Gravatar corbinea2004-02-06
* bugs avec Pose et AssertGravatar barras2004-01-09
* cc updateGravatar corbinea2003-12-09
* error messages adjustementGravatar corbinea2003-12-02
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
* removal of CC.v lemata in cc (deprecated)Gravatar corbinea2003-11-26
* CC: added injection theoryGravatar corbinea2003-11-25
* Code simplification in CCGravatar corbinea2003-11-20
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01