Tachmach.New is now in Proofview.Goal.enter style.

As a result the use of the glist-style interface for manipulating goals has almost been removed.

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

7 files changed, 75 insertions, 92 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 7874f5ac66..f852995a08 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -85,10 +85,12 @@ let elim_res_pf_THEN_i clenv tac gls =
 
 open Proofview.Notations
 let new_elim_res_pf_THEN_i clenv tac =
-  Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) >>= fun clenv' ->
-  Proofview.tclTHEN
-    (Proofview.V82.tactic (clenv_refine false clenv'))
-    (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
+  Proofview.Goal.enter begin fun gl ->
+    let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) gl in
+    Proofview.tclTHEN
+      (Proofview.V82.tactic (clenv_refine false clenv'))
+      (Proofview.tclEXTEND [] (Proofview.tclUNIT()) (Array.to_list (tac clenv')))
+  end
 
 let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index fec2503a9d..2e7ee10bc0 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -354,8 +354,8 @@ 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)
+let enter f = (); fun env rdefs gl info ->
+  f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info) gl
 
 (*** Conversion in goals ***)
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6a19e0d69a..fb6c9ddb1e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -149,7 +149,7 @@ 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
+val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive
 
 (*** Additional functions ***)
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 364cfeb4b5..1e0cc7c24c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -668,12 +668,18 @@ end
 
 module Goal = struct
 
-  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
+  type t = {
+    env : Environ.env;
+    sigma : Evd.evar_map;
+    hyps : Environ.named_context_val;
+    concl : Term.constr ;
+    self : Goal.goal ; (* for compatibility with old-style definitions *)
+  }
+
+  let env { env=env } = env
+  let sigma { sigma=sigma } = sigma
+  let hyps { hyps=hyps } = hyps
+  let concl { concl=concl } = concl
 
   let lift s =
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -694,7 +700,9 @@ module Goal = struct
 
   let return x = lift (Goal.return x)
 
-  let enter_t f = Goal.enter (fun env sigma hyps concl -> f (env,sigma,hyps,concl))
+  let enter_t f = Goal.enter begin fun env sigma hyps concl self ->
+    f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
+  end
   let enter f =
     lift (enter_t f) >= fun ts ->
     tclDISPATCH ts
@@ -702,7 +710,11 @@ module Goal = struct
     lift (enter_t f) >= fun ts ->
     tclDISPATCHL ts >= fun res ->
     tclUNIT (List.flatten res)
-    
+
+
+  (* compatibility *)
+  let goal { self=self } = self
+
 end
 
 module NonLogical = Proofview_monad.NonLogical
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6d5e9d75d0..5051e195a5 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -293,13 +293,15 @@ module Goal : sig
   (* [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
-  
 
   (* [lift (Goal.return x)] *)
   val return : 'a -> 'a glist tactic
   val enter : (t -> unit tactic) -> unit tactic
   val enterl : (t -> 'a glist tactic) -> 'a glist tactic
 
+
+  (* compatibility: avoid if possible *)
+  val goal : t -> Goal.goal
 end
 
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a50c06b39f..8e3ab5975c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -207,65 +207,46 @@ let pr_glls glls =
 module New = struct
   open Proofview.Notations
 
-  let pf_apply f =
-    Proofview.Goal.lift begin
-      Goal.env >- fun env ->
-      Goal.defs >- fun sigma ->
-      Goal.return (f env sigma)
-    end
-
-  let of_old f =
-    Proofview.Goal.lift (Goal.V82.to_sensitive f)
-
-  let pf_global_sensitive id =
-    Goal.hyps >- fun hyps ->
-    let hyps = Environ.named_context_of_val hyps in
-    Goal.return (Constrintern.construct_reference hyps id)
+  let pf_apply f gl =
+    f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+
+  let of_old f gl =
+    f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl }
 
-  let pf_global id =
-    Proofview.Goal.lift (pf_global_sensitive id)
+  let pf_global id gl =
+    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Environ.named_context_of_val hyps in
+    Constrintern.construct_reference hyps id
 
-  let pf_ids_of_hyps_sensitive =
-    Goal.hyps >- fun hyps ->
+  let pf_ids_of_hyps gl =
+    let hyps = Proofview.Goal.hyps gl in
     let hyps = Environ.named_context_of_val hyps in
-    Goal.return (ids_of_named_context hyps)
-  let pf_ids_of_hyps =
-    Proofview.Goal.lift pf_ids_of_hyps_sensitive
-
-  let pf_get_new_id id =
-    Proofview.Goal.lift begin
-      pf_ids_of_hyps_sensitive >- fun ids ->
-      Goal.return (next_ident_away id ids)
-    end
-
-  let pf_get_hyp_sensitive id =
-    Goal.hyps >- fun hyps ->
+    ids_of_named_context hyps
+
+  let pf_get_new_id id gl =
+    let ids = pf_ids_of_hyps gl in
+    next_ident_away id ids
+
+  let pf_get_hyp id gl =
+    let hyps = Proofview.Goal.hyps gl in
     let hyps = Environ.named_context_of_val hyps in
     let sign =
       try Context.lookup_named id hyps
       with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id))
     in
-    Goal.return sign
-  let pf_get_hyp id =
-    Proofview.Goal.lift (pf_get_hyp_sensitive id)
-
-  let pf_get_hyp_typ_sensitive id =
-    pf_get_hyp_sensitive id >- fun (_,_,ty) ->
-    Goal.return ty
-  let pf_get_hyp_typ id =
-    Proofview.Goal.lift (pf_get_hyp_typ_sensitive id)
-
-  let pf_hyps_types =
-    Proofview.Goal.lift begin
-      Goal.env >- fun env ->
-      let sign = Environ.named_context env in
-      Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
-    end
-
-  let pf_last_hyp =
-    Proofview.Goal.lift begin
-      Goal.hyps >- fun hyps ->
-      Goal.return (List.hd (Environ.named_context_of_val hyps))
-    end
+    sign
+
+  let pf_get_hyp_typ id gl =
+    let (_,_,ty) = pf_get_hyp id gl in
+    ty
+
+  let pf_hyps_types gl =
+    let env = Proofview.Goal.env gl in
+    let sign = Environ.named_context env in
+    List.map (fun (id,_,x) -> (id, x)) sign
+
+  let pf_last_hyp gl =
+    let hyps = Proofview.Goal.hyps gl in
+    List.hd (Environ.named_context_of_val hyps)
 
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 7c96bd93bc..1ca15d9ae1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,31 +134,17 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  open Goal
   open Proofview
 
-  val pf_apply : (env -> evar_map -> 'a) -> 'a glist tactic
-  val pf_global_sensitive : identifier -> constr sensitive
-  val pf_global : identifier -> constr glist tactic
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a glist tactic
-
-  val pf_get_new_id  : identifier -> identifier glist tactic
-  val pf_ids_of_hyps_sensitive : identifier list sensitive
-  val pf_ids_of_hyps : identifier list glist tactic
-  val pf_hyps_types : (identifier * types) list glist tactic
-
-  val pf_get_hyp_sensitive : identifier -> named_declaration sensitive
-  val pf_get_hyp : identifier -> named_declaration glist tactic
-  val pf_get_hyp_typ_sensitive : identifier -> types sensitive
-  val pf_get_hyp_typ        : identifier -> types glist tactic
-  val pf_last_hyp           : named_declaration glist tactic
-end
-
-
-
-
-
-
-
+  val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
+  val pf_global : identifier -> Proofview.Goal.t -> constr
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
 
+  val pf_get_new_id  : identifier -> Proofview.Goal.t -> identifier
+  val pf_ids_of_hyps : Proofview.Goal.t -> identifier list
+  val pf_hyps_types : Proofview.Goal.t -> (identifier * types) list
 
+  val pf_get_hyp : identifier -> Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : identifier -> Proofview.Goal.t -> types
+  val pf_last_hyp           : Proofview.Goal.t -> named_declaration
+end