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, 9 insertions, 6 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index dace158ac8..364cfeb4b5 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -668,7 +668,12 @@ end
 
 module Goal = struct
 
-  type 'a u = 'a list
+  type t = Environ.env*Evd.evar_map*Environ.named_context_val*Term.constr
+
+  let env (env,_,_,_) = env
+  let sigma (_,sigma,_,_) = sigma
+  let hyps (_,_,hyps,_) = hyps
+  let concl (_,_,_,concl) = concl
 
   let lift s =
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -688,15 +693,13 @@ module Goal = struct
       tclZERO e
 
   let return x = lift (Goal.return x)
-  let concl = lift Goal.concl
-  let hyps = lift Goal.hyps
-  let env = lift Goal.env
 
+  let enter_t f = Goal.enter (fun env sigma hyps concl -> f (env,sigma,hyps,concl))
   let enter f =
-    lift (Goal.enter f) >= fun ts ->
+    lift (enter_t f) >= fun ts ->
     tclDISPATCH ts
   let enterl f =
-    lift (Goal.enter f) >= fun ts ->
+    lift (enter_t f) >= fun ts ->
     tclDISPATCHL ts >= fun res ->
     tclUNIT (List.flatten res)