aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2003-11-27Ajout ne_stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5002 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Protection contre les notations videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4999 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ↵herbelin
Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4996 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25modif lexer: ident peut commencer par _barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments ↵herbelin
recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4989 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-23Prise en compte des definitions locales dans les (co-)points-fixesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4974 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Suppression des niveaux videsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Ajout Print Implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4961 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21Pas d'entrees autres que les predefinies en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4958 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-20Nouvelle solution pour le probleme d'effacement des niveaux vides de ↵herbelin
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
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵herbelin
dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Protection contre l'effacement des niveaux vides de operconstr et pattern ↵herbelin
par le delete_rule de camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4947 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18reparation bug moins unaire (erreur de PP)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4938 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-17Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4927 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-15Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4920 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Compatibilite %Therbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4906 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Bug parsing castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4899 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13factorisation et generalisation des clausesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Suppression du "..." final !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4880 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la ↵herbelin
bibliotheque standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4867 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-12Idtac peut prendre un argument à affichernarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09'as' avant 'using' dans 'destruct'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4838 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Fusion de tuple_constr/tuple_pattern dans operconstr/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4832 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Added Instantiate ... incorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 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-11-04En v8, une notation, c'est 2 regles et un niveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4795 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Explicitation message d'erreur nombres negatifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4792 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-03Compatibilite V7.4 pour le delimiteur de positiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4782 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-02Le printeur de Show Script n'etait pas le bon en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4775 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4763 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Il ne faut pas mettre le constrarg des tactiques au niveau lconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4762 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Traduction des noms pour les refs de pr_glob_generic (via pr_global)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4760 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Utilisation de niveaux pour l'extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4759 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Extension de get_constr_entry et symbol_of_production pour gerer les ↵herbelin
extensions de la grammaire des motifs de Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4758 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Heritage des notations v7 seulement si zero information v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4749 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout de Print Visibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4733 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Saut de ligne avant les infos non logiques de print_aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4714 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4713 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4712 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Independance de grammar.cmo vis a vis de Searchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4711 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 03:26:40 +0000