aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Collapse)Author
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
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
2000-12-14Amélioration message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1106 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Raffinement erreur Wrong Predicateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1097 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silentfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1086 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-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-05Mini-nettoyage noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 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-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-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-29Suppression cast inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1033 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Now AddRecPath and AddPath can be used with an As option to specify thesacerdot
Coq dir path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1025 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29load_path_entry structure simplified; field relative_subdir renamed to ↵sacerdot
coq_dirpath git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1022 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Ajout d'une option d'alias à -Iherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1016 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un ↵herbelin
chemin Unix à un chemin Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1013 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Remplacement des add_include par add_rec_include pour avoir le repertoire ↵herbelin
dans le nom long git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1008 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath ↵herbelin
pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Distinction local/globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@997 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27uniformisation messages d'erreurfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@993 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des définitions localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@984 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Branchement des Local sur des SectionLocalDefherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@977 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte noms longs dans divers fonctions de Printherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@959 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Remplacement de certains sp_of_id par des locateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@956 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26sp au lieu de id dans END-SECTIONherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@955 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Réorganisation autour de globalize_constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@952 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon ↵filliatr
Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24SearchPattern et SearchRewritefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@943 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24- coqc: utilise le meilleur coq possiblefilliatr
- 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
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Informations inutilesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@925 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@923 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Bug qualidconstarg (intervient pour Transparent)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@921 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Reparation IsMutConstruct + Transparentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵herbelin
'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22retablissement de line_oriented_parser pour Yvesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@915 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Elimination d'un test sur les macrosdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@912 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21implicites manuelsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Begin-End Silent deviennent Set?Unset Silentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@899 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ↵filliatr
variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@897 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Petit bug entre close_section'sherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@894 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte des noms qualifiés dans certaines commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@884 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@883 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Tables séparées pour chaque type de global; calcul de la Nametab de la ↵herbelin
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
2000-11-20Ajout erreur GlobalNotFoundherbelin
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.25.1) at 2026-04-21 18:00:09 +0000