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

7 files changed, 77 insertions, 86 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 5a244fe7d..b5c496e26 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -87,7 +87,7 @@ let contradiction_term (c,lbind as cl) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    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. *)
       let typ = type_of c in
       let _, ccl = splay_prod env sigma typ in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index de4c58371..9c1107beb 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -87,7 +87,7 @@ let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
   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 *)
   let typc = type_of c in
   Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
@@ -99,24 +99,22 @@ let general_decompose recognizer c =
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
-let head_in =
-  Goal.env >- fun env ->
-  Goal.defs >- fun sigma ->
-  Goal.return begin
-    fun indl t ->
-      try
-        let ity,_ =
-          if !up_to_delta
-          then find_mrectype env sigma t
-          else extract_mrectype t
-        in List.mem ity indl
-      with Not_found -> false
-  end
+let head_in indl t gl =
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  try
+    let ity,_ =
+      if !up_to_delta
+      then find_mrectype env sigma t
+      else extract_mrectype t
+    in List.mem ity indl
+  with Not_found -> false
 
 let decompose_these c l =
+  Proofview.Goal.enter begin fun gl ->
   let indl = (*List.map inductive_of*) l in
-  Proofview.Goal.lift head_in >>= fun head_in ->
-  general_decompose (fun (_,t) -> head_in indl t) c
+  general_decompose (fun (_,t) -> head_in indl t gl) c
+  end
 
 let decompose_nonrec c =
   general_decompose
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 284199586..14770af00 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -326,15 +326,15 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
       mkConst c , eff
   | _ -> assert false
 
-let type_of_clause = function
-  | None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl))
-  | Some id -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Tacmach.New.pf_get_hyp_typ id gl))
+let type_of_clause cls gl = match cls with
+  | None -> Proofview.Goal.concl gl
+  | Some id -> Tacmach.New.pf_get_hyp_typ id gl
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.enter begin fun gl ->
   let isatomic = isProd (whd_zeta hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
-  type_of_clause cls >>= fun type_of_cls ->
+  let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun c type_of_cls in
   let (elim,effs) =
     Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) gl
@@ -877,7 +877,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
 
 let onEquality with_evars tac (c,lbindc) =
   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 reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in
   try (* type_of can raise exceptions *)
   let t = type_of c in
@@ -1674,20 +1674,20 @@ let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t)
 let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t)
 
 let rewrite_multi_assumption_cond cond_eq_term cl =
-  let rec arec = function
+  let rec arec hyps gl = match hyps with
     | [] -> error "No such assumption."
     | (id,_,t) ::rest ->
 	begin
 	  try
-            cond_eq_term t >>= fun dir ->
+            let dir = cond_eq_term t gl in
 	    general_multi_rewrite dir false (mkVar id,NoBindings) cl
-	  with | Failure _ | UserError _ -> arec rest
+	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
   Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
     let hyps = Environ.named_context_of_val hyps in
-    arec hyps
+    arec hyps gl
   end
 
 let replace_multi_term dir_opt c  =
@@ -1697,9 +1697,6 @@ let replace_multi_term dir_opt c  =
       | Some true -> cond_eq_term_left c
       | Some false -> cond_eq_term_right c
   in
-  let cond_eq_fun t =
-    Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (cond_eq_fun t gl))
-  in
   rewrite_multi_assumption_cond cond_eq_fun
 
 let _ =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 088ce71d4..e4bcf658b 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -680,10 +680,8 @@ let  mkCaseEq a  : unit Proofview.tactic =
 
 
 let case_eq_intros_rewrite x =
-  Proofview.Goal.lift begin
-    Goal.concl >- fun concl ->
-    Goal.return (nb_prod concl)
-  end >>= fun n ->
+  Proofview.Goal.enter begin fun gl ->
+  let n = nb_prod (Proofview.Goal.concl gl) in
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
@@ -698,6 +696,7 @@ let case_eq_intros_rewrite x =
 		    rewrite_except h]
     end
   ]
+  end
 
 let rec find_a_destructable_match t =
   match kind_of_term t with
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ebccd95b7..725508965 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -463,7 +463,7 @@ let raw_inversion inv_kind id status names =
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
     let reduce_to_atomic_ind = Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind gl in
-    let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+    let type_of = Tacmach.New.pf_type_of gl in
     begin
       try
         Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 265af5b08..224762e0a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -562,11 +562,9 @@ module New = struct
       tac2 id
     end
 
-  let fullGoal =
-    Proofview.Goal.enterl begin fun gl ->
+  let fullGoal gl =
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
-    Proofview.Goal.return (None :: List.map Option.make hyps)
-    end
+    None :: List.map Option.make hyps
 
   let tryAllHyps tac =
     Proofview.Goal.enter begin fun gl ->
@@ -574,8 +572,9 @@ module New = struct
     tclFIRST_PROGRESS_ON tac hyps
     end
   let tryAllHypsAndConcl tac =
-    fullGoal >>= fun fullGoal ->
-    tclFIRST_PROGRESS_ON tac fullGoal
+    Proofview.Goal.enter begin fun gl ->
+      tclFIRST_PROGRESS_ON tac (fullGoal gl)
+    end
 
   let onClause tac cl =
     Proofview.Goal.enter begin fun gl ->
@@ -592,11 +591,7 @@ module New = struct
     let elim = Tacmach.New.of_old (mk_elim ind) gl in
     (* applying elimination_scheme just a little modified *)
     let indclause' = clenv_match_args indbindings indclause in
-    let type_of = Tacmach.New.pf_apply Typing.type_of gl in
-    begin try (* type_of can raise an exception *)
-            Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) gl)
-      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-    end >>= fun elimclause ->
+    let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in
     let indmv =
       match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c317ca0d4..fd14dc938 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -421,23 +421,21 @@ type intro_name_flag =
   | IntroBasedOn of Id.t * Id.t list
   | IntroMustBe of Id.t
 
-let find_name loc decl = function
+let find_name loc decl x gl = match x with
   | IntroAvoid idl ->
       (* this case must be compatible with [find_intro_names] below. *)
-      Goal.env >- fun env ->
-      Goal.defs >- fun sigma ->
-      Goal.V82.to_sensitive (fresh_id idl (default_id env sigma decl))
-  | IntroBasedOn (id,idl) ->  Goal.V82.to_sensitive (fresh_id idl id)
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      Tacmach.New.of_old (fresh_id idl (default_id env sigma decl)) gl
+  | IntroBasedOn (id,idl) ->  Tacmach.New.of_old (fresh_id idl id) gl
   | IntroMustBe id ->
       (* When name is given, we allow to hide a global name *)
-      Goal.hyps >- fun hyps ->
+      let hyps = Proofview.Goal.hyps gl in
       let hyps = Environ.named_context_of_val hyps in
       let ids_of_hyps = ids_of_named_context hyps in
       let id' = next_ident_away id ids_of_hyps in
       if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
-      Goal.return id'
-let find_name loc decl x =
-  Proofview.Goal.lift (find_name loc decl x)
+      id'
 
 (* Returns the names that would be created by intros, without doing
    intros.  This function is supposed to be compatible with an
@@ -464,10 +462,10 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
     let concl = Proofview.Goal.concl gl in
     match kind_of_term concl with
     | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        find_name loc (name,None,t) name_flag >>= fun name ->
+        let name = find_name loc (name,None,t) name_flag gl in
 	build_intro_tac name move_flag tac
     | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
-        find_name loc (name,Some b,t) name_flag >>= fun name ->
+        let name = find_name loc (name,Some b,t) name_flag gl in
 	build_intro_tac name move_flag tac
     | _ ->
 	begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct)
@@ -1420,7 +1418,7 @@ let rewrite_hyp l2r id =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env 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 whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
     try (* type_of can raise an exception *)
       let t = whd_betadeltaiota (type_of (mkVar id)) in
@@ -1967,7 +1965,7 @@ let forward usetac ipat c =
   match usetac with
   | None ->
       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
       begin try (* type_of can raise an exception *)
               let t = type_of c in
               Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
@@ -2206,7 +2204,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
 	      (letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
 	| _ ->
-            let type_of = Tacmach.New.pf_apply Typing.type_of gl in
+            let type_of = Tacmach.New.pf_type_of gl in
 	    let id = id_of_name_using_hdchar (Global.env()) (type_of c)
 		       Anonymous in
             let x = Tacmach.New.of_old (fresh_id [] id) gl in
@@ -3362,7 +3360,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 
 	    | _ ->
                 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 an exception *)
                 let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
@@ -3586,20 +3584,21 @@ let dImp cls =
 let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
 let reflexivity_red allowred =
+  Proofview.Goal.enter begin fun gl ->
   (* PL: usual reflexivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
-  let concl = if not allowred then Goal.concl
+  let concl = if not allowred then Proofview.Goal.concl gl
     else
-      Goal.concl >- fun c ->
-      Goal.env >- fun env ->
-      Goal.defs >- fun sigma ->
-      Goal.return (whd_betadeltaiota env sigma c)
+      let c = Proofview.Goal.concl gl in
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      whd_betadeltaiota env sigma c
   in
-  Proofview.Goal.lift concl >>= fun concl ->
     match match_with_equality_type concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
+  end
 
 let reflexivity =
   Proofview.tclORELSE
@@ -3641,19 +3640,19 @@ let match_with_equation c =
     Proofview.tclZERO NoEquationFound
 
 let symmetry_red allowred =
+  Proofview.Goal.enter begin fun gl ->
   (* PL: usual symmetry don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
   let concl =
     if not allowred then
-      Goal.concl
+      Proofview.Goal.concl gl
     else
-      Goal.concl >- fun c ->
-      Goal.env >- fun env ->
-      Goal.defs >- fun sigma ->
-      Goal.return (whd_betadeltaiota env sigma c)
+      let c = Proofview.Goal.concl gl in
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      whd_betadeltaiota env sigma c
   in
-  Proofview.Goal.lift concl >>= fun concl ->
   match_with_equation concl >= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
@@ -3663,6 +3662,7 @@ let symmetry_red allowred =
           (apply eq_data.sym)
       end
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
+  end
 
 let symmetry =
   Proofview.tclORELSE
@@ -3677,7 +3677,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   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 an exception *)
   let ctype = type_of (mkVar id) in
   let sign,t = decompose_prod_assum ctype in
@@ -3722,41 +3722,42 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_transitivity hdcncl eq_kind t =
-  Proofview.Goal.lift begin match eq_kind with
+  Proofview.Goal.enter begin fun gl ->
+  let (eq1,eq2) = match eq_kind with
   | MonomorphicLeibnizEq (c1,c2) ->
-      Goal.return (mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]))
+      mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
   | PolymorphicLeibnizEq (typ,c1,c2) ->
-      Goal.return (mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]))
+      mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
   | HeterogenousEq (typ1,c1,typ2,c2) ->
-      Goal.env >- fun env ->
-      Goal.defs >- fun sigma ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
       let type_of = Typing.type_of env sigma in
       let typt = type_of t in
-      Goal.return 
         (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
          mkApp(hdcncl, [| typt; t; typ2; c2 |]))
-  end >>= fun (eq1,eq2) ->
+  in
   Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq2))
     (Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq1))
        (Tacticals.New.tclTHENLIST
 	  [ Tacticals.New.tclDO 2 intro;
 	    Tacticals.New.onLastHyp simplest_case;
 	    Proofview.V82.tactic assumption ]))
+  end
 
 let transitivity_red allowred t =
+  Proofview.Goal.enter begin fun gl ->
   (* PL: usual transitivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
   let concl =
     if not allowred then
-      Goal.concl
+      Proofview.Goal.concl gl
     else
-      Goal.concl >- fun c ->
-      Goal.env >- fun env ->
-      Goal.defs >- fun sigma ->
-      Goal.return (whd_betadeltaiota env sigma c)
+      let c = Proofview.Goal.concl gl in
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      whd_betadeltaiota env sigma c
   in
-  Proofview.Goal.lift concl >>= fun concl ->
   match_with_equation concl >= fun with_eqn ->
   match with_eqn with
   | Some eq_data,_,_ ->
@@ -3771,6 +3772,7 @@ let transitivity_red allowred t =
       match t with
       | None -> Proofview.tclZERO (Errors.UserError ("",str"etransitivity not supported for this relation."))
       | Some t -> prove_transitivity eq eq_kind t
+  end
 
 let transitivity_gen t =
   Proofview.tclORELSE