diff options
Diffstat (limited to 'plugins/quote')
| -rw-r--r-- | plugins/quote/quote.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 89d161f73e..532a2f11d6 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -454,8 +454,8 @@ let quote_terms ivs lc = let quote f lid = Proofview.Goal.enter begin fun gl -> - Tacmach.New.pf_global f >>= fun f -> - Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl -> + let f = Tacmach.New.pf_global f gl in + let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs -> let concl = Proofview.Goal.concl gl in Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms -> @@ -469,8 +469,9 @@ let quote f lid = end let gen_quote cont c f lid = - Tacmach.New.pf_global f >>= fun f -> - Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl -> + Proofview.Goal.enter begin fun gl -> + let f = Tacmach.New.pf_global f gl in + let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs -> Proofview.Goal.lift (quote_terms ivs [c]) >>= fun quoted_terms -> let (p, vm) = match quoted_terms with @@ -480,6 +481,7 @@ let gen_quote cont c f lid = match ivs.variable_lhs with | None -> cont (mkApp (f, [| p |])) | Some _ -> cont (mkApp (f, [| vm; p |])) + end (*i |