aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Collapse)Author
2003-05-22Test backtrackingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4062 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Nouveaux testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-27Ce que Try récupèreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3960 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29indentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3811 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Adding tests for the "functional induction" facility.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28MAJ pour Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3596 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵herbelin
une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la ↵desmettr
nouvelle organisation des reels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3424 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02MAJ sur MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3356 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-06Test de la correction d'un bug soumis par Dachuan Yuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3217 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque ↵herbelin
ces hypothèses étaient dépendantes dans d'autres hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3178 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Parenthèses manquantes pour se conformer à la doc (et au nouveau ↵herbelin
PeanoSyntax.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3163 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-22*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2908 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19correction bugs Tautocourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-18*** empty log message ***desmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2900 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05*** empty log message ***corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2839 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-05Added a new uncompleteness bug found in Tauto.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2838 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-14*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2785 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Test de l'interprétation des fermetures de Match Context (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2782 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Test de l'interprétation des fermetures de Match Contextherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2780 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-11Tests pour la tactique Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2777 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07I added a comment on the tactic compute_POS.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2767 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07This example does not work in coq-7.3, but does in coq-7.2.bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2766 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout exemple JCF conflit variable interne, variable de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2764 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Des exemples sérieuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2762 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout exemple Yves renommage différent d'une var de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2759 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2755 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2726 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2500 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2438 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-21Ajout test de Pierre Crégutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2420 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2418 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-18*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2417 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-16Ajout d'un test sur les anonymes dépendant dans des arguments implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2400 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-15Test le filtrage dépendant vers l'avantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2366 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Ajout d'un exemple de Christineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2365 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19MAJ Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2338 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19NatRing (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2326 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19NatRingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2325 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Un peu plus d'inférence des ? traitée par le Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2323 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2297 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-11Test des coercions dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 14:47:07 +0000