aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Bug identarg au lieu de qualidargGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1075 85f007b7-540e-0410-9357-904b9bb8a0f7
* section_path etait en fait bonne dans ast et buggee dans printer.mlGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1074 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1073 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2ème bug de traduction des PathGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug de traduction des PathGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1071 85f007b7-540e-0410-9357-904b9bb8a0f7
* message d'erreurGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1070 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de la syntaxe de LetTacGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout erreur DoesNotOccurInGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppresion de l'option -as, c'est maintenant -R qui devient l'option ↵Gravatar herbelin2000-12-06
| | | | | | 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
* Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le ↵Gravatar herbelin2000-12-06
| | | | | | but et ses hypothèses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Divers bugs LetTacGravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait list_except_assoc qui existe en standard dans ocaml (remove_assoc)Gravatar herbelin2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1063 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1062 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1061 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1060 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour la phase debugageGravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour les qualidconstargGravatar delahaye2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation d'un bug de pretty-printGravatar delahaye2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de quote devant les ident et les ?Gravatar delahaye2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1054 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du répertoire config utilisé par System en localGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug Cases en presence d'une absence de clauseGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte Let dans le calcul des arguments manquants d'un lemme ↵Gravatar herbelin2000-12-05
| | | | | | (clenv_environments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inner types are now reduced and arrows are created whenGravatar sacerdot2000-12-05
| | | | | | | products have dummy binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1050 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mini-nettoyage noms longsGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de ↵Gravatar herbelin2000-12-05
| | | | | | 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
* Nouvelle table de noms pour les locaux qui ne survit pas à la fermeture de ↵Gravatar herbelin2000-12-05
| | | | | | 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
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de constr_of_stringGravatar mohring2000-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Portage d'AutoRewriteGravatar delahaye2000-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1043 85f007b7-540e-0410-9357-904b9bb8a0f7
* LETIN now has a letintarget instead of a targetGravatar sacerdot2000-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1042 85f007b7-540e-0410-9357-904b9bb8a0f7
* cictypes.dtd changedGravatar sacerdot2000-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Used a force function to force stream evaluation only for aestaetics reasons.Gravatar sacerdot2000-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Identifier order in the inner-types file changed.Gravatar sacerdot2000-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de la syntaxe des options -I et -RGravatar herbelin2000-11-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug option -I et -R quand le répertoire est '..'Gravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte REQUIRE dans print_leafGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug option -I et -R quand le répertoire est '.'Gravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de la contrainte de type dans Definition comme étant un ↵Gravatar herbelin2000-11-29
| | | | | | cast de l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression cast inutileGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1033 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout constr_displayGravatar filliatr2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1032 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1031 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajoutGravatar filliatr2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1030 85f007b7-540e-0410-9357-904b9bb8a0f7
* -I configGravatar mohring2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les noms longs (2eme)Gravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1028 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les noms longsGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications due to the new As option in AddPath and AddRecPath.Gravatar sacerdot2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1026 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 09:14:51 +0000