aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egrammar.ml
Commit message (Collapse)AuthorAge
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
| | | | | | | camlp4. Petit nettoyage en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
| | | | | | | | | | | bug "no level labelled 8" (camlp5 ne sait pas annuler un extend lorsque le niveau initial existe mais est vide : l'appel à delete efface le niveau au lieu d'annuler l'effet de extend et de revenir à un niveau existant vide). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité hyp=var dans Tactic Notation + nettoyageGravatar herbelin2006-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9147 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
| | | | | | | | | | | | | | 'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵Gravatar herbelin2005-12-30
| | | | | | de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (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
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affinements suite à extension Tactic Notation aux tacticiellesGravatar herbelin2005-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles + erreur typage TacAlias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7028 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵Gravatar herbelin2005-01-02
| | | | | | printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage d'une bibliothèque de grands entiers naturels vers une ↵Gravatar herbelin2004-12-25
| | | | | | 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@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug Notation: il faut re-déclarer les règles de parsing des ↵Gravatar herbelin2004-11-22
| | | | | | notations au moment de la déclaration d'interprétation car la règle de parsing peut être dans un autre fichier qui n'est pas importé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6340 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de motifs récursifs dans Notation; quelques simplifications ↵Gravatar herbelin2004-03-17
| | | | | | au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'Gravatar herbelin2004-03-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
| | | | | | | | dans le module de leur définition. Error_in_file dans Util et étendu avec possibilité de noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation de qqs bugs du traducteurGravatar barras2004-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
* name_app accessible a tous dans NameopsGravatar herbelin2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle solution pour le probleme d'effacement des niveaux vides de ↵Gravatar herbelin2003-11-20
| | | | | | operconstr et pattern: plus de niveaux vides git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre l'effacement des niveaux vides de operconstr et pattern ↵Gravatar herbelin2003-11-19
| | | | | | par le delete_rule de camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammarGravatar herbelin2003-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4920 85f007b7-540e-0410-9357-904b9bb8a0f7
* En v8, une notation, c'est 2 regles et un niveauGravatar herbelin2003-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extensibilite de la grammaires des patternsGravatar herbelin2003-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4761 85f007b7-540e-0410-9357-904b9bb8a0f7
* On n'autorise plus les niveaux doubles L/R en v8Gravatar herbelin2003-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4670 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage des projections au niveau 1Gravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
* 9 est associatif a gaucheGravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
| | | | | | | | | | | | | | Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Localisation erreurs TacAlias; Globalisation moins tolérante dans lesGravatar herbelin2003-04-28
| | | | | | | définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵Gravatar letouzey2003-04-16
| | | | | | list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte notations dans les extensions de motiffGravatar herbelin2002-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure factorisation des entrées NEXT internesGravatar herbelin2002-12-15
| | | | | | | | Nouvelle entrée "annot" pour contourner le conflit entre ">" et les annotations entre piquants git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3440 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de non-indépendance des règles d'affichage et parsing vis à vis du ↵Gravatar herbelin2002-12-03
| | | | | | nom des variables de la notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7
* On force l'associativité pour les entrées sans niveauxGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Synchro level (suite)Gravatar herbelin2002-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de Snext pour gérer les symboles non associatifsGravatar herbelin2002-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3343 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-05 15:13:32 +0000