From e057d9cb8276d1d727825a940673bfb95660ddf5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 Nov 2013 21:17:01 +0100
Subject: Do not use ugly Dyn features in the Quote plugin. Use instead the
 provided tactic environment to handle open terms.

---
 plugins/quote/g_quote.ml4 | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index abb13efd5c..1f11b07ad9 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,14 +8,22 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Names
+open Misctypes
 open Tacexpr
+open Geninterp
 open Quote
 
-let make_cont k x =
-  let k = TacDynamic(Loc.ghost, Tacinterp.tactic_in (fun _ -> k)) in
-  let x = TacDynamic(Loc.ghost, Pretyping.constr_in x) in
-  let tac = <:tactic<let cont := $k in cont $x>> in
-  Tacinterp.interp tac
+let loc = Loc.ghost
+let cont = (loc, Id.of_string "cont")
+let x = (loc, Id.of_string "x")
+
+let make_cont (k : glob_tactic_expr) (c : Constr.t) =
+  let c = Tacinterp.Value.of_constr c in
+  let tac = TacCall (loc, ArgVar cont, [Reference (ArgVar x)]) in
+  let tac = TacLetIn (false, [(cont, Tacexp k)], TacArg (loc, tac)) in
+  let ist = { lfun = Id.Map.singleton (snd x) c; extra = TacStore.empty; } in
+  Tacinterp.eval_tactic_ist ist tac
 
 TACTIC EXTEND quote
   [ "quote" ident(f) ] -> [ quote f [] ]
-- 
cgit v1.2.3