aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2002-12-12Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...desmettr
2002-12-09Add an example with Ring.bertot
2002-12-02MAJ sur MAJherbelin
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
2002-11-25MAJherbelin
2002-11-24MAJherbelin
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-11-06Test de la correction d'un bug soumis par Dachuan Yuherbelin
2002-10-29Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
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-16Parseur pour n>20 dans nat plus disponibleherbelin
2002-10-06correcting the treatment of many tactics that use quant_hyp in file xlate.mlbertot
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-09-21Changement de sémantique de Remark : maintenant un global comme les autresherbelin
2002-08-21Correctioncoq
2002-08-16Encore quelques tests sur modules...coq
2002-08-15Test for redundant clausesherbelin
2002-08-14Test affichage optimal des coercionsherbelin
2002-08-13Petites corrections ici et lacoq
2002-08-02Modules dans COQ\!\!\!\!coq
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-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
2002-06-14*** empty log message ***herbelin
2002-06-13Test de l'interprétation des fermetures de Match Context (2ème)herbelin
2002-06-13Test de l'interprétation des fermetures de Match Contextherbelin
2002-06-11Tests pour la tactique Regdesmettr
2002-06-07Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputherbelin
2002-06-07I added a comment on the tactic compute_POS.bertot
2002-06-07This example does not work in coq-7.3, but does in coq-7.2.bertot
2002-06-06Ajout exemple JCF conflit variable interne, variable de sectionherbelin
2002-06-06Des exemples sérieuxherbelin
2002-06-06Ajout exemple Yves renommage différent d'une var de sectionherbelin
2002-06-05Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructherbelin
2002-06-03*** empty log message ***herbelin
2002-05-29*** empty log message ***herbelin
2002-04-17Quelques bugs avec inject_natherbelin
2002-04-12*** empty log message ***herbelin
2002-02-28*** empty log message ***herbelin
2002-01-25Test affichage O de nat dans une expression sur Zherbelin
2002-01-25*** empty log message ***herbelin
2002-01-21Ajout test de Pierre Crégutherbelin
2002-01-18*** empty log message ***herbelin
2002-01-18*** empty log message ***herbelin
2002-01-16Ajout d'un test sur les anonymes dépendant dans des arguments implicitesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 02:36:15 +0000