aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Collapse)Author
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
2001-12-19Test sobriété de la réduction de Intuitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2351 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Test sobriété de la réduction de Intuitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2350 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Test syntaxe des constructions de l'état initialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2132 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Commit par erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2129 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Test syntaxe des entiers relatifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2128 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Test syntaxe des réelsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2127 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 18:07:18 +0000