Less use of the list-based interface for goal-bound tactics.

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

5 files changed, 13 insertions, 11 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 1e0cc7c24c..8a3511651f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -548,7 +548,6 @@ let in_proofview p k =
 type 'a glist  = 'a list
 
 module Notations = struct
-  let (>-) = Goal.bind
   let (>=) = tclBIND
   let (>>=) t k =
     t >= fun l ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5051e195a5..207df891e4 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -220,8 +220,6 @@ type 'a glist  = private 'a list
 
 (* Notations for building tactics. *)
 module Notations : sig
-  (* Goal.bind *)
-  val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
 
   (* tclBIND *)
   val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8e3ab5975c..4928ffcfe8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -218,6 +218,11 @@ module New = struct
     let hyps = Environ.named_context_of_val hyps in
     Constrintern.construct_reference hyps id
 
+
+  let pf_type_of gl t =
+    pf_apply type_of gl t
+
+
   let pf_ids_of_hyps gl =
     let hyps = Proofview.Goal.hyps gl in
     let hyps = Environ.named_context_of_val hyps in
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 1ca15d9ae1..48c4f8d48b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -140,6 +140,8 @@ module New : sig
   val pf_global : identifier -> Proofview.Goal.t -> constr
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
 
+  val pf_type_of : Proofview.Goal.t -> Term.constr -> Term.types
+
   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
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index dc48cfc3bc..1cc08fa49b 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -42,22 +42,20 @@ let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
 
 (* Prints the goal *)
 
-let db_pr_goal =
-  let (>>=) = Goal.bind in
-  Goal.env >>= fun env ->
-  Goal.concl >>= fun concl ->
+let db_pr_goal gl =
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
   let penv = print_named_context env in
   let pc = print_constr_env env concl in
-  Goal.return begin
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
-  end
 
 let db_pr_goal =
-  let (>>=) = Proofview.Notations.(>>=) in
-  Proofview.Goal.lift db_pr_goal >>= fun pg ->
+  Proofview.Goal.enter begin fun gl ->
+  let pg = db_pr_goal gl in
   Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
+  end
 
 
 (* Prints the commands *)