aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* [ -d ... ] au lieu de [ -f ... ] sur commit précédéntGravatar herbelin2004-01-01
* Protection contre l'echec des tests parser pour la distribGravatar herbelin2003-12-27
* Suppression en v8Gravatar herbelin2003-12-27
* BUGGravatar herbelin2003-12-24
* Bug commit precedentGravatar herbelin2003-12-23
* Renommages des hypotheses transformees car en raison des possibles dependance...Gravatar herbelin2003-12-23
* ajout test de non-regression Clear d'une def localeGravatar barras2003-12-17
* Ajout exemple YvesGravatar herbelin2003-12-12
* Pour eviter d'avoir un gros type dans SetGravatar herbelin2003-12-05
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
* Simplest Demo on modulesGravatar coq2003-11-28
* removal of CC.v lemata in cc (deprecated)Gravatar corbinea2003-11-26
* CC: added injection theoryGravatar corbinea2003-11-25
* Niveau V8Gravatar herbelin2003-11-13
* Fermeture de la section maintenant necessaireGravatar herbelin2003-11-13
* Passage a un SStream predicatifGravatar herbelin2003-11-13
* Test GeneralizeGravatar herbelin2003-11-09
* MAJGravatar herbelin2003-10-27
* 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