aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Test obsoleteGravatar herbelin2003-10-14
* CleaningGravatar herbelin2003-10-13
* Logic_TypeSyntax disparuGravatar herbelin2003-10-11
* *** empty log message ***Gravatar herbelin2003-10-10
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* 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
* Traduction des tests success et test en v8Gravatar herbelin2003-10-02
* Correction bug 328Gravatar coq2003-09-23
* test d'implicite incorrect depuis que eq porte sur TypeGravatar barras2003-09-23
* L'exemple phare de modules - simplifie pour TPHOLsGravatar coq2003-09-22
* 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
* Corrige Bug (PR#290)Gravatar coq2003-05-05
* Ce que Try récupèreGravatar herbelin2003-04-27
* Débranchement des tests output qui sont faussés par le traducteurGravatar herbelin2003-04-15
* indentationGravatar herbelin2003-03-29
* *** empty log message ***Gravatar barras2003-03-14
* MAJGravatar herbelin2003-03-04
* 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
* commentaireGravatar coq2003-02-06
* MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutGravatar coq2003-01-31
* Pb de parenthèse dans "Check (S (plus O O))"Gravatar herbelin2003-01-30
* MAJ pour RegGravatar desmettr2003-01-28
* *** empty log message ***Gravatar barras2003-01-22
* *** empty log message ***Gravatar herbelin2003-01-20
* Tests ltacGravatar herbelin2003-01-19
* Il ne doit plus y avoir de preuves non terminées à la sortie du fichierGravatar herbelin2003-01-19
* *** empty log message ***Gravatar herbelin2003-01-16
* Problème de désynchronisation des variables du type et du corps d'un point-...Gravatar herbelin2003-01-15
* Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...Gravatar herbelin2003-01-15
* Export M + Module M <: SIGGravatar coq2003-01-09
* Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...Gravatar desmettr2002-12-12
* Add an example with Ring.Gravatar bertot2002-12-09
* MAJ sur MAJGravatar herbelin2002-12-02
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-12-02
* MAJGravatar herbelin2002-11-25
* MAJGravatar herbelin2002-11-24
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-11-24
* Test de la correction d'un bug soumis par Dachuan YuGravatar herbelin2002-11-06
* Des critères plus fins d'analyse des implicites automatiques; meilleur affic...Gravatar herbelin2002-10-29
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:04:17 +0000