diff options
Diffstat (limited to 'plugins/quote/quote.ml')
| -rw-r--r-- | plugins/quote/quote.ml | 6 |
1 files changed, 2 insertions, 4 deletions
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 |