Try to remove intermediate allocations when dealing with goal-specific tactics.

Introduces a primitive Goal.enter which allows to access the common information needed by goal-specific tactics, avoids a number of monadic binds, and some unnecessary allocations of lists.

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

4 files changed, 20 insertions, 1 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index e590e7763b..46f002cb3e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -352,6 +352,9 @@ let env env _ _ _ = env
 let defs _ rdefs _ _ =
   !rdefs
 
+let enter f = (); fun env rdefs _ info ->
+  f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info)
+
 (*** Conversion in goals ***)
 
 let convert_hyp check (id,b,bt as d) env rdefs gl info =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 216e12f3a2..6a19e0d69a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -147,6 +147,9 @@ val env : Environ.env sensitive
 (* [defs] is the [Evd.evar_map] at the current evaluation point *)
 val defs : Evd.evar_map sensitive
 
+(* [enter] combines [env], [defs], [hyps] and [concl] in a single
+   primitive. *)
+val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a) -> 'a sensitive
 
 (*** Additional functions ***)
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index fb8796dbd5..dace158ac8 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -691,8 +691,19 @@ module Goal = struct
   let concl = lift Goal.concl
   let hyps = lift Goal.hyps
   let env = lift Goal.env
+
+  let enter f =
+    lift (Goal.enter f) >= fun ts ->
+    tclDISPATCH ts
+  let enterl f =
+    lift (Goal.enter f) >= fun ts ->
+    tclDISPATCHL ts >= fun res ->
+    tclUNIT (List.flatten res)
+    
 end
 
 module NonLogical = Proofview_monad.NonLogical
 
 let tclLIFT = Proofview_monad.Logical.lift
+
+
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 3f80768d83..fa1a8d56f7 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -290,7 +290,9 @@ module Goal : sig
 
   (* [lift (Goal.return x)] *)
   val return : 'a -> 'a glist tactic
-  (* [lift Goal.concl] *)    
+  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