aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Collapse)Author
2006-09-23Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderherbelin
leading to wrong/failing printing of notations such as "- 1" or "1 -"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9167 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23- Correction filtrage des notations impliquant un "match" : la présenceherbelin
des localisations empêchait toute unification des pattern de filtrage de réussir. - Ajout au passage d'unification des pattern modulo alpha. - Exemples dans Notations.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9163 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Adaptation Tactics.out et Cases.out au comportement actuel à défaut ↵herbelin
d'éviter l'affichage de trop d'espacements dans Tactics et de prendre une décision sur le rôle du _ dans Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8935 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-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-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-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-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-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-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
2004-12-27Ajout test bug 860herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6513 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Ajout d'une version nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6451 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09MAJ avec les particularités de l'afficheur v7 de la V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6450 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Test d'affichage d'un Fix donné avec /nherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6449 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Fichier non traductible (référence à des objets invisibles ce qui ↵herbelin
empêche de traduire Locate) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6448 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Intégré à Implicit.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6447 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Ajout suffixe 8 pour test en nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6446 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Plus de statut spécial pour Remarkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6445 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Désactivation du test du printer arithmétique v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6442 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Test lieurs dans Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6309 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17test-suite/output/Notations.outherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6308 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Ajout tests affichage coercions vers Funclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5788 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4585 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-04MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3731 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-19Il ne doit plus y avoir de preuves non terminées à la sortie du fichierherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3538 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3516 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-15Problème de désynchronisation des variables du type et du corps d'un ↵herbelin
point-fixe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3504 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-09Export M + Module M <: SIGcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3276 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3271 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-29Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3191 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-16Parseur pour n>20 dans nat plus disponibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3152 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-21Changement de sémantique de Remark : maintenant un global comme les autresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3028 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-21Correctioncoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2976 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-14Test affichage optimal des coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2967 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2802 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-07Locate n'échoue plus: déplacement de Remark1 et Remark2 dans outputherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2768 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2750 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2726 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Quelques bugs avec inject_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2653 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-01-25Test affichage O de nat dans une expression sur Zherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2440 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 11:40:31 +0000