aboutsummaryrefslogtreecommitdiff
path: root/parsing/astterm.ml
AgeCommit message (Collapse)Author
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur ↵herbelin
affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3164 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
référence donnée git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ↵herbelin
hack temporaire autour du printer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3120 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-14Utilisation d'une construction spéciale SECVAR pour gérer laherbelin
globalisation des variables de section (en espérant plus de robustesse vis à vis des bugs récurrents de Infix pour les variables avec implicites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2684 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-10Plus de souplesse pour les constructeurs encapsulés sous des définitionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2674 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-18Suppression d'un warning plus surprenant qu'utileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2658 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-10Syntactic Definition autorisée dans les motifs de Cases (utile notammentherbelin
pour fusionner eq et eqT) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2628 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 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-15Nouvelle correction du bug confusion entre implicites de locaux et de globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2115 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Bug collision entre les implicites d'un global et les variables locales de ↵herbelin
même nom court git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2108 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-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21Mise en place globalisation optionnelle pour Infix/Distfixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2046 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵herbelin
des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1946 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1938 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-06-18Interpretation MetaId + Progress + Instdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1789 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
n'etaient pas affiches correctement lors du Save si on les avait donne en argument de tactique. Avec Bruno, nous avons simplifie l'ast en remplacant les MLCASE NOREC et autres CASE NOREC par des choses plus simples. Il y a maintenant un noeud LET, un IF, un CASE et un MATCH qui sont a peu pres semblables mais qui permettent de se souvenir quoi afficher. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1781 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-29Facilites pour le debogguage des univers.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25message d'erreur pour rattrapper l'anomalie avec SQUASHbarras
Check {True}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1719 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-24Messages d'erreur Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1703 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-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1447 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@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-08Simplificationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1358 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au ↵herbelin
reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1330 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Bug localisation des Syntactif Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1303 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-19Autour des quotations avec Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1258 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Suppression warning variable de filtrage en majusculeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1175 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Amélioration message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1108 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bug dans les alias de Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1095 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-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-21Prise en compte des implicites dans les regles de grammairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@895 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Acceptation des noms qualifiés; utilisation de global_reference dans ↵herbelin
pattern; prise en compte des noms qualifiés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@881 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:01:48 +0000