aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-12-11Debut de reparation de simplmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1083 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-09tests automatiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1082 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-07type attribute added to PROD (for ForAll vs Pi rendering)sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1081 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-07COPYRIGHT file added; some comments changedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1080 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06*** empty log message ***sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1079 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Modif rapide pour prise en compte eqTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1078 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Prise en compte `?' dans les `` ``herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1077 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06MAJ nom long de eqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1076 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Bug identarg au lieu de qualidargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1075 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06section_path etait en fait bonne dans ast et buggee dans printer.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1074 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1073 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-062ème bug de traduction des Pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1072 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Bug de traduction des Pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1071 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1070 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1069 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Extension de la syntaxe de LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1068 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Ajout erreur DoesNotOccurInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1067 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Suppresion de l'option -as, c'est maintenant -R qui devient l'option ↵herbelin
standard pour associer un nom physique à un nom logique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1066 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le ↵herbelin
but et ses hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1065 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Divers bugs LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1064 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Retrait list_except_assoc qui existe en standard dans ocaml (remove_assoc)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1063 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1062 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1061 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1060 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06*** empty log message ***mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1059 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Pour la phase debugagemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1058 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-06Correction pour les qualidconstargdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1056 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Reparation d'un bug de pretty-printdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1055 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Plus de quote devant les ident et les ?delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1054 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Ajout du répertoire config utilisé par System en localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1053 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Bug Cases en presence d'une absence de clauseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1052 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Prise en compte Let dans le calcul des arguments manquants d'un lemme ↵herbelin
(clenv_environments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1051 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Inner types are now reduced and arrows are created whensacerdot
products have dummy binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1050 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1049 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Mini-nettoyage noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de ↵herbelin
la section; 2 racines officielles pour l'espace des noms : Coq et Scratch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1047 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de ↵herbelin
la section : utilisée pour les variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1046 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-04caractere opaque des constantes repris en comptefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1045 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-04Ajout de constr_of_stringmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1044 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-02Portage d'AutoRewritedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1043 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-01LETIN now has a letintarget instead of a targetsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1042 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-01cictypes.dtd changedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1041 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-30Used a force function to force stream evaluation only for aestaetics reasons.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1040 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-30Identifier order in the inner-types file changed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1039 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-30Changement de la syntaxe des options -I et -Rherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1038 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Bug option -I et -R quand le répertoire est '..'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1037 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Prise en compte REQUIRE dans print_leafherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1036 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Bug option -I et -R quand le répertoire est '.'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1035 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Prise en compte de la contrainte de type dans Definition comme étant un ↵herbelin
cast de l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1034 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:19:55 +0000