aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
AgeCommit message (Collapse)Author
2001-11-29reparation de Locatebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Romegamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Affichage des dir_path videherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2006 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Romega/names/Makefilemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-04erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1920 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-10Parsingherbelin
- Typage renforcé dans les grammaires (distinction des vars et des metavars) - Disparition de SLAM au profit de ABSTRACT - Paths primitifs dans les quotations (syntaxe concrète à base de .) - Mise en place de identifier dès le type ast - Protection de identifier contre les effets de bord via un String.copy - Utilisation de module_ident (= identifier) dans les dir_path (au lieu de string) Table des noms qualifiés - Remplacement de la table de visibilité par une table qui ne cache plus les noms de modules et sections mais seulement les noms des constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel module A déjà existant : seuls les noms de constructions de l'ancien A qui existent aussi dans le nouveau A seront cachés) - Renoncement à la possibilité d'accéder les formes non déchargées des constantes définies à l'intérieur de sections et simplification connexes (suppression de END-SECTION, une seule table de noms qui ne survit pas au discharge) - Utilisation de noms longs pour les modules, de noms qualifiés pour Require and co, tests de cohérence; pour être cohérent avec la non survie des tables de noms à la sortie des section, les require à l'intérieur d'une section eux aussi sont refaits à la fermeture de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-01Ajout add_prefix/add_suffixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1868 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Ajout d'espace dans les règles d'affichage des infix si des lettres ↵herbelin
figurent dans le token git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7
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
2000-12-25Alias variable_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Le bon choix, c'est finalement identifier = stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1132 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Mise en place d'un module Ident avec test de l'efficacité quand ↵herbelin
identifier=string git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1130 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-11-29Ajout d'un test pour vérifier qu'on a affaire à un identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1012 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-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-23Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@929 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-20Introduction constant_path = section_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@870 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Bug sur précédent commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@819 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Nettoyage Names suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@818 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵herbelin
DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03bug make_strength reparefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@200 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02modifs pour premiere edition de liensfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01diverses fonctions ajouteesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@170 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-19 - un effort sur la doc (ocamlweb)filliatr
- module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-10modules System, Lib et Statesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-09les sections ne sont plus stockées à l'envers dans les section pathsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@70 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-18module Reduction (debut)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-17generic, term et evdfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-16Initial revisionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 05:39:40 +0000