aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Parseur pour n>20 dans nat plus disponibleGravatar herbelin2002-10-16
* correcting the treatment of many tactics that use quant_hyp in file xlate.mlGravatar bertot2002-10-06
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01
* Encore quelques rangements dans Nametab + petits trucsGravatar coq2002-09-27
* Changement de sémantique de Remark : maintenant un global comme les autresGravatar herbelin2002-09-21
* CorrectionGravatar coq2002-08-21
* Encore quelques tests sur modules...Gravatar coq2002-08-16
* Test for redundant clausesGravatar herbelin2002-08-15
* Test affichage optimal des coercionsGravatar herbelin2002-08-14
* Petites corrections ici et laGravatar coq2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* *** 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
* Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementGravatar filliatr2002-06-21
* *** 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
* Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputGravatar herbelin2002-06-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 20:30:34 +0000