More Proofview.Goal.enter.

Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.

This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.

This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.

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

1 files changed, 12 insertions, 10 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index bf061095c8..89d161f73e 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -453,18 +453,20 @@ let quote_terms ivs lc =
   yet. *)
 
 let quote 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.lift (compute_ivs f cl) >>= fun ivs ->
-  Proofview.Goal.concl >>= fun concl ->
-  Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
-  let (p, vm) = match quoted_terms with
-    | [p], vm -> (p,vm)
-    | _ -> assert false
-  in
-  match ivs.variable_lhs with
+  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 ->
+    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 ->
+    let (p, vm) = match quoted_terms with
+      | [p], vm -> (p,vm)
+      | _ -> assert false
+    in
+    match ivs.variable_lhs with
     | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
     | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+  end
 
 let gen_quote cont c f lid =
   Tacmach.New.pf_global f >>= fun f ->