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

2 files changed, 19 insertions, 14 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)
     
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index fa1a8d56f7..6d5e9d75d0 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -283,6 +283,13 @@ end
 
 module Goal : sig
 
+  type t
+
+  val concl : t -> Term.constr
+  val hyps : t -> Environ.named_context_val
+  val env : t -> Environ.env
+  val sigma : t -> Evd.evar_map
+
   (* [lift_sensitive s] returns the list corresponding to the evaluation
      of [s] on each of the focused goals *)
   val lift : 'a Goal.sensitive -> 'a glist tactic
@@ -290,14 +297,9 @@ module Goal : sig
 
   (* [lift (Goal.return x)] *)
   val return : 'a -> 'a glist tactic
-  val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> unit tactic) -> unit tactic
-  val enterl : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a glist tactic) -> 'a glist tactic
-  (* [lift Goal.concl] *)
-  val concl : Term.constr glist tactic
-  (* [lift Goal.hyps] *)
-  val hyps : Environ.named_context_val glist tactic
-  (* [lift Goal.env] *)
-  val env : Environ.env glist tactic
+  val enter : (t -> unit tactic) -> unit tactic
+  val enterl : (t -> 'a glist tactic) -> 'a glist tactic
+
 end