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, 24 insertions, 20 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 7bd0c7e43d..aee7efb76d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -798,16 +798,18 @@ let ltac_ring_structure e =
 open Proofview.Notations
 
 let ring_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  try (* find_ring_strucure can raise an exception *)
-    let rl = make_args_list rl t in
-    let e = find_ring_structure env sigma rl in
-    let rl = carg (make_term_list e.ring_carrier rl) in
-    let lH = carg (make_hyp_list env lH) in
-    let ring = ltac_ring_structure e in
-    ltac_apply f (ring@[lH;rl])
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try (* find_ring_strucure can raise an exception *)
+      let rl = make_args_list rl t in
+      let e = find_ring_structure env sigma rl in
+      let rl = carg (make_term_list e.ring_carrier rl) in
+      let lH = carg (make_hyp_list env lH) in
+      let ring = ltac_ring_structure e in
+      ltac_apply f (ring@[lH;rl])
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
@@ -1121,16 +1123,18 @@ let ltac_field_structure e =
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
 let field_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  try
-    let rl = make_args_list rl t in
-    let e = find_field_structure env sigma rl in
-    let rl = carg (make_term_list e.field_carrier rl) in
-    let lH = carg (make_hyp_list env lH) in
-    let field = ltac_field_structure e in
-    ltac_apply f (field@[lH;rl])
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try
+      let rl = make_args_list rl t in
+      let e = find_field_structure env sigma rl in
+      let rl = carg (make_term_list e.field_carrier rl) in
+      let lH = carg (make_hyp_list env lH) in
+      let field = ltac_field_structure e in
+      ltac_apply f (field@[lH;rl])
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 
 TACTIC EXTEND field_lookup