aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Declare Implicit TacticGravatar herbelin2005-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression test CCSolve car remplaçé par Congruence mais qui ne traite ↵Gravatar herbelin2005-09-09
| | | | | | pas les connecteurs propositionnels (pour Pierre C.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7359 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test clear final dans intros patternGravatar herbelin2005-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Consequence of allowing the numerical argument of auto to be an ident for ltacGravatar herbelin2005-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7062 85f007b7-540e-0410-9357-904b9bb8a0f7
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
| | | | | | | | convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Unset Implicit Arguments manquantGravatar herbelin2005-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵Gravatar herbelin2005-03-20
| | | | | | hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test bug #935Gravatar herbelin2005-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6843 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers temporairesGravatar herbelin2005-02-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6769 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2005-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug #922Gravatar herbelin2005-02-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6729 85f007b7-540e-0410-9357-904b9bb8a0f7
* test de la bonne position des vars de ltac entre les vars et les relsGravatar herbelin2005-02-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6664 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new tutorial on (co)inductive types by Pierre Casteran.Gravatar sacerdot2005-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test bug 860Gravatar herbelin2004-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réactivation des tests output avec test aussi de la nouvelle syntaxeGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une version nouvelle syntaxeGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6451 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ avec les particularités de l'afficheur v7 de la V8Gravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test d'affichage d'un Fix donné avec /nGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fichier non traductible (référence à des objets invisibles ce qui ↵Gravatar herbelin2004-12-09
| | | | | | empêche de traduire Locate) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégré à Implicit.vGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout suffixe 8 pour test en nouvelle syntaxeGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de statut spécial pour RemarkGravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Désactivation du test du printer arithmétique v7Gravatar herbelin2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug do_restrict_hypGravatar herbelin2004-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur commit précédentGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #888Gravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #889Gravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Failed in 8.0pl1Gravatar herbelin2004-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Was failing in 8.0pl1Gravatar herbelin2004-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6393 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression bruit perlGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-commit version nouvelle syntaxeGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à la v8 pour test parserGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test lieurs dans NotationGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6309 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite/output/Notations.outGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test dependent rewriteGravatar herbelin2004-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6260 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2004-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6225 85f007b7-540e-0410-9357-904b9bb8a0f7
* reflexivity, symmetry, symmetry ... in e transitivity now fall-backGravatar sacerdot2004-10-14
| | | | | | | to their setoid_* counterparts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
* New commandsGravatar sacerdot2004-10-07
| | | | | | | | | | | | | 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
* Added "as ..." parameter to Add Morphism.Gravatar sacerdot2004-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added "as ..." parameters to "Add Setoid"Gravatar sacerdot2004-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6169 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tacticGravatar sacerdot2004-09-30
| | | | | | | | 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
* New tactic [setoid_]rewrite ... in ... [generate side conditions ...].Gravatar sacerdot2004-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test updated.Gravatar sacerdot2004-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6150 85f007b7-540e-0410-9357-904b9bb8a0f7
* AjoutsGravatar herbelin2004-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #255Gravatar herbelin2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6127 85f007b7-540e-0410-9357-904b9bb8a0f7
* * New test (for setoid_replace in the general case)Gravatar sacerdot2004-09-03
| | | | | | | * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 21:39:33 +0000