aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2006-04-28Ajout bug #1102herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8761 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24Timide tentative de clarification du statut de l'opérateur de filtrageherbelin
PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-15Tests notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8720 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-15Test synchronisation chargement objets non logiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8719 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22- Correction bug calcul mind_consnrealargs, introduit à la révisionherbelin
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
2006-03-05Ajout test relatif au bug #984herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8127 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-02Ajout test bug 1089herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8113 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-02Correction du bug 808: il est maintenant interdit de déclarer une ↵coq
assomption en cours de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8107 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Prise en compte coercions autour des sous-termes filtrés (si non dépendants)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7961 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-23Répercussion mise à jour de Pierre Casteran vis à vis du changement de ↵herbelin
statut du paramètre de Acc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7921 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-20Test bug 983herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7901 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-15Test utf-8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7868 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Test conflictuel - ajouté pour mémoireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7849 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Test or-patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7848 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Ajout test notation récursiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7847 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05Test choix conflit afficheur de nombres selon la présence ou pas d'une coercionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-02Affichage de 'O' (lettre) comme '0' (chiffre)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Test bug #1025herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7765 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-27Mini-test d'extractionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7743 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Achèvement suppression traducteur dans contrib/interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7738 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-23Test printing of Tactic Notation which was broken until dec 2005herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7707 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Abandon tests syntaxe v7 (correction)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7704 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22option '-top dir' now works also in batch mode; it is even necessary to ↵herbelin
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
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Abandon tests syntaxe v7; ajouts tests modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7692 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21MAJ syntaxe v7 avant activation en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7689 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Activation du test de Refine en v7 pour mémoire avant passage à la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7688 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Anciennement déplacé dans 'output'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7687 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21cf ltac4.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7686 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-18L'option -no-vm laisse la place à une option -vmherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7667 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-03*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7498 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-03deplacement params_indmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7497 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Test reproductibilité du bug #1031herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7491 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Ajout tests interactifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7489 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-01Interactive test of Backherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7486 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Declare Implicit Tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7366 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Suppression test CCSolve car remplaçé par Congruence mais qui ne traite ↵herbelin
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
2005-09-08Test clear final dans intros patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7356 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-23Consequence of allowing the numerical argument of auto to be an ident for ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7062 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
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
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7034 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-21Ajout Unset Implicit Arguments manquantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6872 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-20Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des ↵herbelin
hyps dépendantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6867 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-19Ajout test bug #935herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6859 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-17Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6850 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16Nouvelle syntaxe 'with' des modules non gérée en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6843 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-08Fix bug #931: leave dependent evars as such for refineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6812 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:07:12 +0000