diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-14 16:43:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-14 17:06:50 +0200 |
| commit | 16675c67c56456f6082c4da7c7657aaa2b1da375 (patch) | |
| tree | a6ef17fecebd140ed7b8cda8082897503f0b40f1 | |
| parent | 5b1a15b5c561ed02335050f45ad123f8d548cee4 (diff) | |
Moving the tactic-in-term extension from G_constr to G_ltac.
| -rw-r--r-- | ltac/g_ltac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 3 |
2 files changed, 8 insertions, 4 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 7fdfc452d..788ba3b8e 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -19,6 +19,7 @@ open Genredexpr open Tok (* necessary for camlp4 *) open Pcoq +open Pcoq.Constr open Pcoq.Vernac_ open Pcoq.Prim open Pcoq.Tactic @@ -83,7 +84,8 @@ let warn_deprecated_appcontext = GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint - tactic_mode constr_may_eval constr_eval selector toplevel_selector; + tactic_mode constr_may_eval constr_eval selector toplevel_selector + operconstr; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -344,6 +346,11 @@ GEXTEND Gram tac = Pcoq.Tactic.tactic -> Vernacexpr.HintsExtern (n,c, in_tac tac) ] ] ; + operconstr: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> + let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in + CHole (!@loc, None, IntroAnonymous, Some arg) ] ] + ; END open Constrarg diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 7021e5270..ccc7c55a8 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -215,9 +215,6 @@ GEXTEND Gram CGeneralization (!@loc, Implicit, None, c) | "`("; c = operconstr LEVEL "200"; ")" -> CGeneralization (!@loc, Explicit, None, c) - | IDENT "ltac"; ":"; "("; tac = Tactic.tactic_expr; ")" -> - let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in - CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; record_declaration: |