Tachmach.New is now in Proofview.Goal.enter style.

As a result the use of the glist-style interface for manipulating goals has almost been removed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 4 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 89d161f73..532a2f11d 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