diff options
Diffstat (limited to 'plugins/quote')
-rw-r--r-- | plugins/quote/g_quote.mlg (renamed from plugins/quote/g_quote.ml4) | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.mlg index 09209dc22..749903c3a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Names open Tacexpr @@ -16,8 +18,12 @@ open Quote open Stdarg open Tacarg +} + DECLARE PLUGIN "quote_plugin" +{ + let cont = Id.of_string "cont" let x = Id.of_string "x" @@ -27,12 +33,14 @@ let make_cont (k : Val.t) (c : EConstr.t) = let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) +} + TACTIC EXTEND quote - [ "quote" ident(f) ] -> [ quote f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +| [ "quote" ident(f) ] -> { quote f [] } +| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } | [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f [] ] + { gen_quote (make_cont k) c f [] } | [ "quote" ident(f) "[" ne_ident_list(lc) "]" "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f lc ] + { gen_quote (make_cont k) c f lc } END |