aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
| | | | | | | | | | | | 7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test relatif au bug #984Gravatar herbelin2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test bug 1089Gravatar herbelin2006-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 808: il est maintenant interdit de déclarer une ↵Gravatar coq2006-03-02
| | | | | | assomption en cours de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte coercions autour des sous-termes filtrés (si non dépendants)Gravatar herbelin2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Répercussion mise à jour de Pierre Casteran vis à vis du changement de ↵Gravatar herbelin2006-01-23
| | | | | | statut du paramètre de Acc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug 983Gravatar herbelin2006-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7901 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test utf-8Gravatar herbelin2006-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test conflictuel - ajouté pour mémoireGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test or-patternsGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test notation récursiveGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test choix conflit afficheur de nombres selon la présence ou pas d'une coercionGravatar herbelin2006-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage de 'O' (lettre) comme '0' (chiffre)Gravatar herbelin2006-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test bug #1025Gravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mini-test d'extractionGravatar herbelin2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test printing of Tactic Notation which was broken until dec 2005Gravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7 (correction)Gravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
* option '-top dir' now works also in batch mode; it is even necessary to ↵Gravatar herbelin2005-12-22
| | | | | | ensure that loaded vernac definitions are defined inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7700 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abandon tests syntaxe v7; ajouts tests modulesGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7692 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ syntaxe v7 avant activation en syntaxe v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Activation du test de Refine en v7 pour mémoire avant passage à la v8Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Anciennement déplacé dans 'output'Gravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7687 85f007b7-540e-0410-9357-904b9bb8a0f7
* cf ltac4.vGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7686 85f007b7-540e-0410-9357-904b9bb8a0f7
* L'option -no-vm laisse la place à une option -vmGravatar herbelin2005-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7667 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2005-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7498 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement params_indGravatar mohring2005-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test reproductibilité du bug #1031Gravatar herbelin2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout tests interactifsGravatar herbelin2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Interactive test of BackGravatar herbelin2005-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7486 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 18:42:16 +0000