diff options
| author | herbelin | 2000-11-20 08:42:15 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-20 08:42:15 +0000 |
| commit | d9c0b901668ccb2c576e7bc314c16b665311a90f (patch) | |
| tree | 88f1e5172244e6c7a8e595bc881172632f3592e7 | |
| parent | c5b51f01ae1c04b9f32c120e4e9f78b36877b3c7 (diff) | |
Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme METAIDENT pour les $id; nouvelle entrée pour les noms qualifiés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@864 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_basevernac.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index ff6b3e24d5..efe9d77cd2 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -81,7 +81,7 @@ GEXTEND Gram <:ast< (LocateFile $f) >> | IDENT "Locate"; IDENT "Library"; id = identarg; "." -> <:ast< (LocateLibrary $id) >> - | IDENT "Locate"; id = identarg; "." -> + | IDENT "Locate"; id = Tactic.qualidarg; "." -> <:ast< (Locate $id) >> (* For compatibility (now turned into a table) *) @@ -206,10 +206,12 @@ GEXTEND Gram | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";"; "." -> <:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >> + + (* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *) | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string; - p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >> + p = Tactic.qualidarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >> | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string; - p = identarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >> + p = Tactic.qualidarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >> (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] @@ -237,7 +239,7 @@ GEXTEND Gram ; production_item: [[ s = STRING -> <:ast< ($STR $s) >> - | nt = non_terminal; po = OPT [ "("; p = Prim.ident; ")" -> p ] -> + | nt = non_terminal; po = OPT [ "("; p = Prim.metaident; ")" -> p ] -> match po with | Some p -> <:ast< (NT $nt $p) >> | _ -> <:ast< (NT $nt) >> ]] |