aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2004-11-28Passage à la v8 pour test parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6367 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Test lieurs dans Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6309 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17test-suite/output/Notations.outherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6308 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Ajout test dependent rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6260 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6225 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-14reflexivity, symmetry, symmetry ... in e transitivity now fall-backsacerdot
to their setoid_* counterparts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-07New commandssacerdot
setoid_reflexivity setoid_symmetry setoid_transitivity The command setoid_symmetry in ... is not implemented yet (it behaves just as symmetry in ... for now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6193 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-04Added "as ..." parameter to Add Morphism.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6176 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01Added "as ..." parameters to "Add Setoid"sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6169 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30New tacticsacerdot
setoid_replace ... with ... in ... [using relation ...] [generate side conditions ...] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6166 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30New tactic [setoid_]rewrite ... in ... [generate side conditions ...].sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29Test updated.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6150 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-25Ajoutsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6136 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24Ajout bug #255herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6127 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03* New test (for setoid_replace in the general case)sacerdot
* Comments/to do changed (but still in italian) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6052 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03* setoid_test.v removed and added again in new syntaxsacerdot
* setoid_test.v8 ported to the new implementation of setoid_*. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6051 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23The previous test file was truncated. New commit to fix the previoussacerdot
commit error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6020 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Several tests for the bug-fixed and improved new version ofsacerdot
setoid_{replace,rewrite}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5973 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5789 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Ajout tests affichage coercions vers Funclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5788 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Ajout testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5787 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-20Protection du destruct pour vérifier que ce n'est pas une anomalie, à ↵herbelin
défaut de faire réussir la tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5754 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-03Points-fixes avec let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5722 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-02Ajout test bug 711herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5720 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-29Test bug 705herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5712 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-28Ajout test If nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5708 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14Ajout exemple Brunoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5673 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5572 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5555 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24bug de PP des fix (coqbugs #574)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5550 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-13Nouvel exemple; correction du contexte du précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5475 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Correctionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Test l'interprétation des scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5460 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout exemple Instherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5459 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout vieil exemple de coq-clubherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout d'un vieil exemple de N. Magaudherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5457 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-11Ajout bug #540herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5452 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-06the output the parser should produce nowbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5438 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-06changed the test for obj_magic.v to be less sensitive to changesbertot
nobody was paying attention anyway git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5437 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Exemple de Fredericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-27Ajout test synthese du predicat a partir du cast d'un filtrage avec dependancesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5390 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
more functions (higher order and polymorphic functions), the principle is a bit better. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5310 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-06Test dependencies in constructorsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5304 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-06Ajout filtrage sur motifs dépendants dans des inductifs différentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5302 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04Vérification de la prise en compte des termes de type non inductifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5294 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-01[ -d ... ] au lieu de [ -f ... ] sur commit précédéntherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5166 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-27Protection contre l'echec des tests parser pour la distribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5157 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-27Suppression en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5156 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:45:01 +0000