aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Les params d'inductif deviennent en même temps propre à chaque inductif ↵Gravatar herbelin2000-12-14
| | | | | | d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message d'erreurGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement erreur Wrong PredicateGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1097 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silentGravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1086 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
* 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
* 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
* 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
* 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
* 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
* Suppression cast inutileGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now AddRecPath and AddPath can be used with an As option to specify theGravatar sacerdot2000-11-29
| | | | | | | Coq dir path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1025 85f007b7-540e-0410-9357-904b9bb8a0f7
* load_path_entry structure simplified; field relative_subdir renamed to ↵Gravatar sacerdot2000-11-29
| | | | | | coq_dirpath git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option d'alias à -IGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ↵Gravatar herbelin2000-11-29
| | | | | | chemin Unix à un chemin Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des add_include par add_rec_include pour avoir le repertoire ↵Gravatar herbelin2000-11-28
| | | | | | dans le nom long git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte du repertoire dans le section path; utilisation de dirpath ↵Gravatar herbelin2000-11-28
| | | | | | pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction local/globalGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@997 85f007b7-540e-0410-9357-904b9bb8a0f7
* uniformisation messages d'erreurGravatar filliatr2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des définitions localesGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement des Local sur des SectionLocalDefGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte noms longs dans divers fonctions de PrintGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de certains sp_of_id par des locateGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@956 85f007b7-540e-0410-9357-904b9bb8a0f7
* sp au lieu de id dans END-SECTIONGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation autour de globalize_constrGravatar herbelin2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
* certains effets disparaissent a la sortie des sections, d'autres non (selon ↵Gravatar filliatr2000-11-24
| | | | | | Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@943 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coqc: utilise le meilleur coq possibleGravatar filliatr2000-11-24
| | | | | | | | - coqc -v réparé - coqtop: options -byte et -opt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@940 85f007b7-540e-0410-9357-904b9bb8a0f7
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Informations inutilesGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@925 85f007b7-540e-0410-9357-904b9bb8a0f7
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug qualidconstarg (intervient pour Transparent)Gravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@921 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵Gravatar herbelin2000-11-22
| | | | | | 'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination d'un test sur les macrosGravatar delahaye2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@912 85f007b7-540e-0410-9357-904b9bb8a0f7
* implicites manuelsGravatar filliatr2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Begin-End Silent deviennent Set?Unset SilentGravatar mohring2000-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@899 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation calcul des implicites et declaration des constantes / inductifs / ↵Gravatar filliatr2000-11-21
| | | | | | variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit bug entre close_section'sGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des noms qualifiés dans certaines commandesGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte noms longsGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tables séparées pour chaque type de global; calcul de la Nametab de la ↵Gravatar herbelin2000-11-20
| | | | | | section; une capsule pour save_module_to git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@860 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 06:58:13 +0000