aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Test obsoleteGravatar herbelin2003-10-14
* Logic_TypeSyntax disparuGravatar herbelin2003-10-11
* Cacher les .v8Gravatar herbelin2003-10-10
* Teste interaction ltac et modulesGravatar herbelin2003-10-08
* Ajout exemple parametres implicitesGravatar herbelin2003-10-08
* Test ConjectureGravatar herbelin2003-10-08
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Correction bug 328Gravatar coq2003-09-23
* Check local definitions in context of inductive typesGravatar herbelin2003-09-06
* ProjectionsGravatar herbelin2003-09-03
* Added a test for Functional Induction.Gravatar courtieu2003-06-21
* Test backtrackingGravatar herbelin2003-05-22
* Nouveaux testsGravatar herbelin2003-05-21
* Ce que Try récupèreGravatar herbelin2003-04-27
* indentationGravatar herbelin2003-03-29
* fixing a typo in the new Funinv.v test in test-suite/successGravatar courtieu2003-02-28
* Adding tests for the "functional induction" facility.Gravatar bertot2003-02-27
* MAJ pour RegGravatar desmettr2003-01-28
* *** empty log message ***Gravatar barras2003-01-22
* Il ne doit plus y avoir de preuves non terminées à la sortie du fichierGravatar herbelin2003-01-19
* Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...Gravatar herbelin2003-01-15
* Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...Gravatar desmettr2002-12-12
* MAJ sur MAJGravatar herbelin2002-12-02
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-12-02
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-11-24
* Test de la correction d'un bug soumis par Dachuan YuGravatar herbelin2002-11-06
* Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...Gravatar herbelin2002-10-23
* Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...Gravatar herbelin2002-10-21
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01
* Encore quelques rangements dans Nametab + petits trucsGravatar coq2002-09-27
* *** empty log message ***Gravatar desmettr2002-07-22
* correction bugs TautoGravatar courant2002-07-19
* *** empty log message ***Gravatar desmettr2002-07-18
* *** empty log message ***Gravatar corbinea2002-07-05
* Added a new uncompleteness bug found in Tauto.Gravatar corbinea2002-07-05
* *** empty log message ***Gravatar herbelin2002-06-14
* Test de l'interprétation des fermetures de Match Context (2ème)Gravatar herbelin2002-06-13
* Test de l'interprétation des fermetures de Match ContextGravatar herbelin2002-06-13
* Tests pour la tactique RegGravatar desmettr2002-06-11
* I added a comment on the tactic compute_POS.Gravatar bertot2002-06-07
* This example does not work in coq-7.3, but does in coq-7.2.Gravatar bertot2002-06-07
* Ajout exemple JCF conflit variable interne, variable de sectionGravatar herbelin2002-06-06
* Des exemples sérieuxGravatar herbelin2002-06-06
* Ajout exemple Yves renommage différent d'une var de sectionGravatar herbelin2002-06-06
* Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructGravatar herbelin2002-06-05
* *** empty log message ***Gravatar herbelin2002-05-29
* *** empty log message ***Gravatar herbelin2002-02-28
* *** empty log message ***Gravatar herbelin2002-01-25
* Ajout test de Pierre CrégutGravatar herbelin2002-01-21
* *** empty log message ***Gravatar herbelin2002-01-18