From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- plugins/quote/g_quote.ml4 | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 79c429615..40c1028e5 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -23,7 +23,6 @@ let cont = Id.of_string "cont" let x = Id.of_string "x" let make_cont (k : Val.t) (c : EConstr.t) = - let c = EConstr.Unsafe.to_constr c in let c = Tacinterp.Value.of_constr c in let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in @@ -33,8 +32,8 @@ 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) (EConstr.of_constr 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) (EConstr.of_constr c) f lc ] + [ gen_quote (make_cont k) c f lc ] END -- cgit v1.2.3