aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_zsyntax.ml
AgeCommit message (Collapse)Author
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
Idea: make coqtop more independant of the standard library. In the future, we can imagine loading the syntax for numerals right after their definition. For the moment, it is easier to stay lazy and load the syntax plugins slightly before the definitions. After this commit, the main (sole ?) references to theories/ from the core ml files are in Coqlib (but many parts of coqlib are only used by plugins), and it mainly concerns Init (+ Logic/JMeq and maybe a few others). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-16Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)letouzey
This way, no more references to NBinDefs.N when doing "Print N". Long-term migration to theories/Numbers is still planned, but it needs more works, for instance to adapt both positive and N and Z at once. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-07Replaced BinNat with a new version that is based on ↵emakarov
theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Branchement sur nouvelle interface de declare_numeral_interpreterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7988 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7818 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵herbelin
reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17Bug affichage entiers négatifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6726 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une ↵herbelin
bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-10Correction bug #868herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6292 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter ↵herbelin
les numeraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4866 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Interpretation des entiers dans N (ex-entier), maj du module des positiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selonherbelin
l'option v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4385 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12MAJ module requis pour le parsing des numérauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4377 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Pas de 0 dans positiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3438 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-25Z dans les patterns via les scopesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3280 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Installation des printers de nombres pour constr_exprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3268 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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
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-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-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Mise en place de parseurs avec globalisation pas seulement dans les ↵herbelin
quotations, pour utilisation par les règles de syntaxe et grammaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@718 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03compilation nativefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:18:38 +0000