aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2003-12-27Suppression en v8herbelin
2003-12-24BUGherbelin
2003-12-23Bug commit precedentherbelin
2003-12-23Renommages des hypotheses transformees car en raison des possibles dependance...herbelin
2003-12-12Ajout exemple Yvesherbelin
2003-12-05Pour eviter d'avoir un gros type dans Setherbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
2003-11-25CC: added injection theorycorbinea
2003-11-13Niveau V8herbelin
2003-11-13Fermeture de la section maintenant necessaireherbelin
2003-11-13Passage a un SStream predicatifherbelin
2003-11-09Test Generalizeherbelin
2003-10-27MAJherbelin
2003-10-14Test obsoleteherbelin
2003-10-11Logic_TypeSyntax disparuherbelin
2003-10-10Cacher les .v8herbelin
2003-10-08Teste interaction ltac et modulesherbelin
2003-10-08Ajout exemple parametres implicitesherbelin
2003-10-08Test Conjectureherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-09-23Correction bug 328coq
2003-09-06Check local definitions in context of inductive typesherbelin
2003-09-03Projectionsherbelin
2003-06-21Added a test for Functional Induction.courtieu
2003-05-22Test backtrackingherbelin
2003-05-21Nouveaux testsherbelin
2003-04-27Ce que Try récupèreherbelin
2003-03-29indentationherbelin
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
2003-02-27Adding tests for the "functional induction" facility.bertot
2003-01-28MAJ pour Regdesmettr
2003-01-22*** empty log message ***barras
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...herbelin
2002-12-12Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...desmettr
2002-12-02MAJ sur MAJherbelin
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-11-06Test de la correction d'un bug soumis par Dachuan Yuherbelin
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...herbelin
2002-10-21Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...herbelin
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-07-22*** empty log message ***desmettr
2002-07-19correction bugs Tautocourant
2002-07-18*** empty log message ***desmettr
2002-07-05*** empty log message ***corbinea
2002-07-05Added a new uncompleteness bug found in Tauto.corbinea
2002-06-14*** empty log message ***herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-12 13:14:20 +0000