aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* commentaireGravatar herbelin2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout tests affichage coercions vers FunclassGravatar herbelin2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout testsGravatar herbelin2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection du destruct pour vérifier que ce n'est pas une anomalie, à ↵Gravatar herbelin2004-05-20
| | | | | | 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
* Points-fixes avec let-inGravatar herbelin2004-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5722 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test bug 711Gravatar herbelin2004-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug 705Gravatar herbelin2004-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test If nouvelle syntaxeGravatar herbelin2004-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5708 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exemple BrunoGravatar herbelin2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5673 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5572 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5555 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de PP des fix (coqbugs #574)Gravatar barras2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvel exemple; correction du contexte du précédentGravatar herbelin2004-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5475 85f007b7-540e-0410-9357-904b9bb8a0f7
* CorrectionsGravatar herbelin2004-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test l'interprétation des scopesGravatar herbelin2004-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exemple InstGravatar herbelin2004-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout vieil exemple de coq-clubGravatar herbelin2004-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un vieil exemple de N. MagaudGravatar herbelin2004-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5457 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #540Gravatar herbelin2004-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5452 85f007b7-540e-0410-9357-904b9bb8a0f7
* the output the parser should produce nowGravatar bertot2004-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5438 85f007b7-540e-0410-9357-904b9bb8a0f7
* changed the test for obj_magic.v to be less sensitive to changesGravatar bertot2004-03-06
| | | | | | | nobody was paying attention anyway git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5437 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exemple de FredericGravatar herbelin2004-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test synthese du predicat a partir du cast d'un filtrage avec dependancesGravatar herbelin2004-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5390 85f007b7-540e-0410-9357-904b9bb8a0f7
* New version of Functional Scheme and functional induction. Deals withGravatar coq2004-02-09
| | | | | | | | 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
* Test dependencies in constructorsGravatar herbelin2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout filtrage sur motifs dépendants dans des inductifs différentsGravatar herbelin2004-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification de la prise en compte des termes de type non inductifGravatar herbelin2004-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5294 85f007b7-540e-0410-9357-904b9bb8a0f7
* [ -d ... ] au lieu de [ -f ... ] sur commit précédéntGravatar herbelin2004-01-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5166 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre l'echec des tests parser pour la distribGravatar herbelin2003-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5157 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression en v8Gravatar herbelin2003-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5156 85f007b7-540e-0410-9357-904b9bb8a0f7
* BUGGravatar herbelin2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug commit precedentGravatar herbelin2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages des hypotheses transformees car en raison des possibles ↵Gravatar herbelin2003-12-23
| | | | | | 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
* ajout test de non-regression Clear d'une def localeGravatar barras2003-12-17
| | | | | | | reparation bug affichage des clauses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5108 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exemple YvesGravatar herbelin2003-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour eviter d'avoir un gros type dans SetGravatar herbelin2003-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5071 85f007b7-540e-0410-9357-904b9bb8a0f7
* ground->firstorder, cc-> congruence, CC final commitGravatar corbinea2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplest Demo on modulesGravatar coq2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7
* removal of CC.v lemata in cc (deprecated)Gravatar corbinea2003-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
* CC: added injection theoryGravatar corbinea2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Niveau V8Gravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fermeture de la section maintenant necessaireGravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage a un SStream predicatifGravatar herbelin2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test GeneralizeGravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4837 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test obsoleteGravatar herbelin2003-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4634 85f007b7-540e-0410-9357-904b9bb8a0f7
* CleaningGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Logic_TypeSyntax disparuGravatar herbelin2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 02:27:26 +0000