diff options
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 9 |
2 files changed, 5 insertions, 6 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0fe0ac42b1..6eeae925a3 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -215,7 +215,7 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | "ltac:"; "("; tac = Tactic.tactic_expr; ")" -> + | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in CHole (!@loc, None, IntroAnonymous, Some arg) ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 0a11d3928a..45d2a09e73 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -111,8 +111,6 @@ GEXTEND Gram | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (g,n,l) | st = simple_tactic -> st - | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(!@loc,ConstrMayEval(ConstrTerm c)) | a = tactic_top_or_arg -> TacArg(!@loc,a) | r = reference; la = LIST0 tactic_arg -> TacArg(!@loc,TacCall (!@loc,r,la)) ] @@ -140,9 +138,7 @@ GEXTEND Gram ; (* Tactic arguments *) tactic_arg: - [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | "ltac:"; n = natural -> TacGeneric (genarg_of_int n) - | a = tactic_top_or_arg -> a + [ [ a = tactic_top_or_arg -> a | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) @@ -151,6 +147,9 @@ GEXTEND Gram (* Can be used as argument and at toplevel in tactic expressions. *) tactic_top_or_arg: [ [ IDENT "uconstr"; ":" ; c = uconstr -> UConstr c + | IDENT "constr"; ":"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) + | IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a + | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> TacGeneric (genarg_of_ipattern ipat) | c = constr_eval -> ConstrMayEval c |