aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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
2003-12-24BUGherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5150 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Bug commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5132 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Renommages des hypotheses transformees car en raison des possibles ↵herbelin
dependances, il n'y a pas de garantie de pouvoir les effacer pour garder le meme nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5131 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-17ajout test de non-regression Clear d'une def localebarras
reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-12Ajout exemple Yvesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5091 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-05Pour eviter d'avoir un gros type dans Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5071 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-28Simplest Demo on modulescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25CC: added injection theorycorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Niveau V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Fermeture de la section maintenant necessaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4893 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Passage a un SStream predicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4891 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Test Generalizeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4837 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4718 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Test obsoleteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4634 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Cleaningherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4616 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11Logic_TypeSyntax disparuherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4558 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Teste interaction ltac et modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4552 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Ajout exemple parametres implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4551 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 03:23:09 +0000