aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Collapse)Author
2001-01-27Ajout alias mutual_inductive_path = section_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1282 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1279 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-25Remplacement d'un bug non documente par un autre documente dans ↵herbelin
quantify_extra_hyps ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1277 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Réorganisation suite ajout de constantes locales dans les Recordsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1268 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25find_section_variable : un traducteur id -> sp pour variables de section; ↵herbelin
variable_strength change de type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1204 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Test pour empêcher 2 sections de même nomsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert ↵herbelin
afin de pouvoir re-rendre visible des noms ayant été cachés depuis l'ouverture du module; renommage de open_module en import_module avec cette nouvelle spéc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1164 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Pédagogieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1152 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Réparation de bugs de LoadPathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1123 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bug des locaux au premier niveau des modules qui disparaissaient de ↵herbelin
l'environnement (changement de is_section_p) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1120 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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-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-11-29load_path_entry structure simplified; field relative_subdir renamed to coq_dirpasacerdot
th; add_path now checks for directory existence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1024 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29La zone par défaut pour le nommage des modules est Scratchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1018 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Enregistrement des racines de la bibliothèqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1014 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-28Les variables doivent persister dans les vo pour HELMherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1007 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-27load_module / open_module un tantinet plus rapidesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@992 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Bug dans find_common_hyps_then_abstract en présence de défs localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@987 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Bug extract_instance en présence de défs localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@985 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des let in dans les instances de globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@976 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@967 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Calcul du chemin optimal dans qualid_of_globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@961 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte de noms absolus dans la nametab + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@958 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@957 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Bug relocation des hypothèses quand les contextes de définitions et ↵herbelin
d'utilisation diffèrent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@953 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-24synchronisation Requirefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@941 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Fonction qualid_of_global pour affichage des paths avec des '.'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@927 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-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-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-22Reparation bug mutuels indmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21reset_name: try / with juste autour de find_entry_p (=> propage lesfilliatr
vraies erreurs de reset_to s'il y en a) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@908 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21ajout d'un frozen_state après la fermeture d'une section (sinon bug !)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@906 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-21correction bug Resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@898 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-20Ajout implicits_of_global + accès par noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@888 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Open est maintenant géré par Nametabherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@869 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Nouveaux points d'accès pour les noms qualifiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@868 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 07:37:27 +0000