aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/cc
Commit message (Expand)AuthorAge
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
* fixed (PR#1483)Gravatar corbinea2007-05-24
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* added congruence improvementGravatar corbinea2006-09-19
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Messages de idtac et fail peuvent maintenant être des listes de string, int ...Gravatar herbelin2006-01-21
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* new congruenceGravatar corbinea2005-08-17
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* Uniformisation de destApplication en destAppGravatar herbelin2005-02-12
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Nouvelle en-têteGravatar herbelin2004-07-16
* oopsGravatar corbinea2004-03-15
* minor changesGravatar corbinea2004-03-14
* congruence now handles disequalitiesGravatar corbinea2004-03-14
* 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
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
* just forgot something in previous commitGravatar corbinea2003-11-26
* 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
* Cacher les .v8Gravatar herbelin2003-10-03
* Ground and CCsolve updatesGravatar corbinea2003-05-25
* 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