diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 3 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 12 |
5 files changed, 13 insertions, 16 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0e7c92a6ce..f5ea021d49 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -142,10 +142,7 @@ GEXTEND Gram [ [ "_" -> (loc, Anonymous) ] ] ; global: - [ [ r = Prim.reference -> r - - (* This is used in quotations *) - | id = METAIDENT -> Ident (loc,id_of_string id) ] ] + [ [ r = Prim.reference -> r ] ] ; constr_pattern: [ [ c = constr -> c ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c0fd07c175..c541b5a7e7 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -95,6 +95,8 @@ GEXTEND Gram TacArg (TacExternal (loc,com,req,la)) | st = simple_tactic -> TacAtom (loc,st) | a = may_eval_arg -> TacArg(a) + | IDENT "constr"; ":"; id = METAIDENT -> + TacArg(MetaIdArg (loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c)) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> @@ -125,7 +127,7 @@ GEXTEND Gram | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) - | id = METAIDENT -> MetaIdArg (loc,id) + | id = METAIDENT -> MetaIdArg (loc,true,id) | "()" -> TacVoid ] ] ; may_eval_arg: @@ -148,7 +150,7 @@ GEXTEND Gram | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: - [ [ id = METAIDENT -> MetaIdArg (loc,id) + [ [ id = METAIDENT -> MetaIdArg (loc,true,id) | n = integer -> Integer n | "()" -> TacVoid ] ] ; diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5d59a8489c..b26f8c77ed 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -383,7 +383,8 @@ let parse_after_dot bp c = let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$'; len = ident_tail (store 0 '$') >] ep -> + | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); + len = ident_tail (store 0 c) >] ep -> comment_stop bp; (("METAIDENT", get_buff len), (bp,ep)) | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 55c6a4387e..2a46388c39 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -957,7 +957,8 @@ let rec pr_tac inherited tac = and pr_tacarg = function | TacDynamic (loc,t) -> pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>")) - | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s)) + | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s)) + | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s)) | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat | TacVoid -> str "()" | Reference r -> pr_ref r diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index e698a187c9..6313a553e6 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -470,19 +470,15 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacFun ($mlexpr_of_list mlexpr_of_ident_option idol$, $mlexpr_of_tactic body$) >> -(* - | Tacexpr.TacFunRec of $dloc$ * identifier * tactic_fun_ast -*) -(* - | Tacexpr.TacArg (Tacexpr.AstTacArg (Coqast.Nmeta $dloc$ id)) -> anti loc id -*) - | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,id)) -> anti loc id + | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id | Tacexpr.TacArg t -> <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >> | _ -> failwith "Quotation of tactic expressions: TODO" and mlexpr_of_tactic_arg = function - | Tacexpr.MetaIdArg (loc,id) -> anti loc id + | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id + | Tacexpr.MetaIdArg (loc,false,id) -> + <:expr< Tacexpr.ConstrMayEval (Rawterm.ConstrTerm $anti loc id$) >> | Tacexpr.TacCall (loc,t,tl) -> <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> | Tacexpr.Tacexp t -> |