From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- plugins/quote/quote.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 87276f5df..edf34607b 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -459,8 +459,7 @@ let quote f lid = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let f = Tacmach.New.pf_global f gl in - let f = EConstr.of_constr f in - let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in let ivs = compute_ivs f cl gl in let concl = Proofview.Goal.concl gl in let quoted_terms = quote_terms env sigma ivs [concl] in @@ -478,8 +477,7 @@ let gen_quote cont c f lid = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let f = Tacmach.New.pf_global f gl in - let f = EConstr.of_constr f in - let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in let ivs = compute_ivs f cl gl in let quoted_terms = quote_terms env sigma ivs [c] in let (p, vm) = match quoted_terms with -- cgit v1.2.3