aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2006-06-06+ ameliorating the tactic "functional induction"jforest
+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8885 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8884 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Adaptation au passage de sig2 dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8870 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Adaptation au passage de vector dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8869 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28Adaptation au passage de option dans Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8868 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-22encore un exemple ne marchant pas, ni avec omega ni avec romegaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8839 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-19tests de Romegaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8832 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-13Correction trou de typage des éliminations d'inductifs introduit dans ↵herbelin
commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-10Conformité nouveaux principes: Declare Module non utilisable pour définir ↵herbelin
un module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8801 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-10Centralisation de la détection lettre/symbole par le lexeur dans les plages ↵herbelin
unicode; ajout de nouvelles plages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8800 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-05Vieux bug de fin 2004 gardé pour mémoireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8792 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-13 02:23:07 +0000