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, 10 insertions, 8 deletions

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