diff options
author | 2019-02-02 19:29:28 -0500 | |
---|---|---|
committer | 2019-02-02 19:29:28 -0500 | |
commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /plugins/quote/g_quote.mlg | |
parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
Diffstat (limited to 'plugins/quote/g_quote.mlg')
-rw-r--r-- | plugins/quote/g_quote.mlg | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/plugins/quote/g_quote.mlg b/plugins/quote/g_quote.mlg new file mode 100644 index 00000000..749903c3 --- /dev/null +++ b/plugins/quote/g_quote.mlg @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +{ + +open Ltac_plugin +open Names +open Tacexpr +open Geninterp +open Quote +open Stdarg +open Tacarg + +} + +DECLARE PLUGIN "quote_plugin" + +{ + +let cont = Id.of_string "cont" +let x = Id.of_string "x" + +let make_cont (k : Val.t) (c : EConstr.t) = + let c = Tacinterp.Value.of_constr c in + let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in + 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) "in" constr(c) "using" tactic(k) ] -> + { 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 } +END |