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

3 files changed, 10 insertions, 16 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0d12388146..32e6d914f9 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -247,7 +247,7 @@ let _M =mkMeta
 
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+  let type_of = Tacmach.New.pf_type_of gl in
   try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> Proofview.V82.tactic (exact_check c)
@@ -473,7 +473,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
 let f_equal =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+    let type_of = Tacmach.New.pf_type_of gl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         let ty = Termops.refresh_universes (type_of c1) in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index a647238bf8..4d6f7b21f3 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1653,7 +1653,7 @@ let onClearedName2 id tac =
 
 let destructure_hyps =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+  let type_of = Tacmach.New.pf_type_of gl in
   let decidability = Tacmach.New.of_old decidability gl in
   let pf_nf = Tacmach.New.of_old pf_nf gl in
     let rec loop = function
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 532a2f11d6..21b221318e 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -220,17 +220,16 @@ let compute_rhs bodyi index_of_f =
 
 (*s Now the function [compute_ivs] itself *)
 
-let compute_ivs f cs =
+let compute_ivs f cs gl =
   let cst = try destConst f with DestKO -> i_can't_do_that () in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
-        Goal.env >- fun env ->
-        Goal.defs >- fun sigma ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         let is_conv = Reductionops.is_conv env sigma in
-        Goal.return
           begin match decomp_term body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
               let n_lhs_rhs = ref []
@@ -394,9 +393,6 @@ module Constrhash = Hashtbl.Make
   [lc: constr list]\\
   [gl: goal sigma]\\ *)
 let quote_terms ivs lc =
-  (* spiwack: [Goal.return () >- fun () -> … ] suspends the effects in
-     [Coqlib.check_required_library]. *)
-  Goal.return () >- fun () ->
   Coqlib.check_required_library ["Coq";"quote";"Quote"];
   let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
@@ -443,10 +439,8 @@ let quote_terms ivs lc =
     auxl ivs.normal_lhs_rhs
   in
   let lp = List.map aux lc in
-  Goal.return begin
     (lp, (btree_of_array (Array.of_list (List.rev !varlist))
             ivs.return_type ))
-  end
 
 (*s actually we could "quote" a list of terms instead of a single
   term. Ring for example needs that, but Ring doesn't use Quote
@@ -456,9 +450,9 @@ let quote f lid =
   Proofview.Goal.enter begin fun gl ->
     let f = Tacmach.New.pf_global f gl in
     let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
-    Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
+    let ivs = compute_ivs f cl gl in
     let concl = Proofview.Goal.concl gl in
-    Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
+    let quoted_terms = quote_terms ivs [concl] in
     let (p, vm) = match quoted_terms with
       | [p], vm -> (p,vm)
       | _ -> assert false
@@ -472,8 +466,8 @@ let gen_quote cont c f lid =
   Proofview.Goal.enter begin fun gl ->
   let f = Tacmach.New.pf_global f gl in
   let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
-  Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
-  Proofview.Goal.lift (quote_terms ivs [c]) >>= fun quoted_terms ->
+  let ivs = compute_ivs f cl gl in
+  let quoted_terms = quote_terms ivs [c] in
   let (p, vm) = match quoted_terms with
     | [p], vm -> (p,vm)
     | _ -> assert false