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

13 files changed, 411 insertions, 239 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 728eaa3fe6..29381c7c82 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1278,7 +1278,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
       ( Proofview.Goal.enter begin fun gl ->
           let sigma = Proofview.Goal.sigma gl in
           let env = Proofview.Goal.env gl in
-          Tacmach.New.pf_last_hyp >>= fun hyp ->
+          let hyp = Tacmach.New.pf_last_hyp gl in
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
       end)
@@ -1376,20 +1376,24 @@ let make_db_list dbnames =
   List.map lookup dbnames
 
 let trivial ?(debug=Off) lems dbnames =
+  Proofview.Goal.enter begin fun gl ->
   let db_list = make_db_list dbnames in
   let d = mk_trivial_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
+  let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
   new_tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
+  end
 
 let full_trivial ?(debug=Off) lems =
+  Proofview.Goal.enter begin fun gl ->
   let dbs = !searchtable in
   let dbs = String.Map.remove "v62" dbs in
   let db_list = List.map snd (String.Map.bindings dbs) in
   let d = mk_trivial_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
+  let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
   new_tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
+  end
 
 let gen_trivial ?(debug=Off) lems = function
   | None -> full_trivial ~debug lems
@@ -1423,8 +1427,10 @@ let extend_local_db gl decl db =
 
 let intro_register dbg kont db =
   Tacticals.New.tclTHEN (dbg_intro dbg)
-    (Tacmach.New.of_old extend_local_db >>= fun extend_local_db ->
-      Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)))
+    (Proofview.Goal.enter begin fun gl ->
+      let extend_local_db = Tacmach.New.of_old extend_local_db gl in
+      Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
+    end)
 
 (* n is the max depth of search *)
 (* local_db contains the local Hypotheses *)
@@ -1452,12 +1458,13 @@ let search d n mod_delta db_list local_db =
 let default_search_depth = ref 5
 
 let delta_auto ?(debug=Off) mod_delta n lems dbnames =
-  Proofview.tclUNIT () >= fun () -> (* delay for the side effects *)
+  Proofview.Goal.enter begin fun gl ->
   let db_list = make_db_list dbnames in
   let d = mk_auto_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
+  let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
   new_tclTRY_dbg d
     (search d n mod_delta db_list hints)
+  end
 
 let auto ?(debug=Off) n = delta_auto ~debug false n
 
@@ -1466,13 +1473,15 @@ let new_auto ?(debug=Off) n = delta_auto ~debug true n
 let default_auto = auto !default_search_depth [] []
 
 let delta_full_auto ?(debug=Off) mod_delta n lems =
+  Proofview.Goal.enter begin fun gl ->
   let dbs = !searchtable in
   let dbs = String.Map.remove "v62" dbs in
   let db_list = List.map snd (String.Map.bindings dbs) in
   let d = mk_auto_dbg debug in
-  Tacmach.New.of_old (make_local_hint_db false lems) >>= fun hints ->
+  let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
   new_tclTRY_dbg d
     (search d n mod_delta db_list hints)
+  end
 
 let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
 let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 9c1f462bac..da8f2668b8 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -113,8 +113,9 @@ let autorewrite ?(conds=Naive) tac_main lbas =
       (Proofview.tclUNIT()) lbas))
 
 let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
+ Proofview.Goal.enter begin fun gl ->
  (* let's check at once if id exists (to raise the appropriate error) *)
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive idl) >>= fun _ ->
+ let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
  let general_rewrite_in id =
   let id = ref id in
   let to_be_cleared = ref false in
@@ -155,6 +156,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
     (List.fold_left (fun tac bas ->
        Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas)))
    idl
+ end
 
 let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]
 
@@ -179,8 +181,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
 	   | None ->
 		 (* try to rewrite in all hypothesis
 		    (except maybe the rewritten one) *)
-                 Tacmach.New.pf_ids_of_hyps >>= fun ids ->
-		 try_do_hyps (fun id -> id)  ids)
+               Proofview.Goal.enter begin fun gl ->
+                 let ids = Tacmach.New.pf_ids_of_hyps gl in
+		 try_do_hyps (fun id -> id)  ids
+               end)
 
 let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT())
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c500a5969d..5a244fe7d5 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -62,11 +62,11 @@ let contradiction_context =
 	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type u ->
 	      (Proofview.tclORELSE
-                 begin
-                   Tacmach.New.pf_apply is_conv_leq >>= fun is_conv_leq ->
+                 (Proofview.Goal.enter begin fun gl ->
+                   let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
 	           filter_hyp (fun typ -> is_conv_leq typ t)
 		     (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
-                 end
+                 end)
                  begin function
 	           | Not_found -> seek_neg rest
                    | e -> Proofview.tclZERO e
@@ -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
-    Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+    let type_of = Tacmach.New.pf_apply Typing.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 b9f077aa46..de4c583715 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -86,7 +86,8 @@ let tmphyp_name = Id.of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  Proofview.Goal.enter begin fun gl ->
+  let type_of = Tacmach.New.pf_apply Typing.type_of gl in
   try (* type_of can raise exceptions *)
   let typc = type_of c in
   Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc))
@@ -96,6 +97,7 @@ let general_decompose recognizer c =
 	      (fun id -> Proofview.V82.tactic (clear [id]))));
        Proofview.V82.tactic (exact_no_check c) ]
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let head_in =
   Goal.env >- fun env ->
@@ -169,8 +171,9 @@ let induction_trailer abs_i abs_j bargs =
           ))
 
 let double_ind h1 h2 =
-  Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) >>= fun abs_i ->
-  Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) >>= fun abs_j ->
+  Proofview.Goal.enter begin fun gl ->
+  let abs_i = Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) gl in
+  let abs_j = Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) gl in
   let abs =
     if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
     if abs_i > abs_j then  Proofview.tclUNIT (abs_j,abs_i) else
@@ -182,6 +185,7 @@ let double_ind h1 h2 =
            Tacticals.New.elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j))
              ([],[]) (mkVar id))))
+  end
 
 let h_double_induction = double_ind
 
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index a0e8fcb884..ee398a8b40 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -120,12 +120,16 @@ let match_eqdec c =
 (* /spiwack *)
 
 let solveArg eqonleft op a1 a2 tac =
-  Tacmach.New.of_old (fun g -> pf_type_of g a1) >>= fun rectype ->
-  Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) >>= fun decide ->
+  Proofview.Goal.enter begin fun gl ->
+  let rectype = Tacmach.New.of_old (fun g -> pf_type_of g a1) gl in
+  let decide =
+    Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) gl
+  in
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
     else [diseqCase eqonleft;eqCase tac;default_auto] in
   (Tacticals.New.tclTHENS (Proofview.V82.tactic (h_elim_type decide)) subtacs)
+  end
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
@@ -160,7 +164,7 @@ let decideGralEquality =
       Proofview.Goal.enter begin fun gl ->
         let concl = Proofview.Goal.concl gl in
         match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
-        Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
+        let headtyp = Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) gl in
         begin match kind_of_term headtyp with
         | Ind mi -> Proofview.tclUNIT mi
         | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
@@ -179,20 +183,24 @@ let decideGralEquality =
 let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality
 
 let decideEquality rectype =
-  Tacmach.New.of_old (mkGenDecideEqGoal rectype) >>= fun decide ->
+  Proofview.Goal.enter begin fun gl ->
+  let decide = Tacmach.New.of_old (mkGenDecideEqGoal rectype) gl in
   (Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide)) [default_auto;decideEqualityGoal])
+  end
 
 
 (* The tactic Compare *)
 
 let compare c1 c2 =
-  Tacmach.New.of_old (fun g -> pf_type_of g c1) >>= fun rectype ->
-  Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) >>= fun decide ->
+  Proofview.Goal.enter begin fun gl ->
+  let rectype = Tacmach.New.of_old (fun g -> pf_type_of g c1) gl in
+  let decide = Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) gl in
   (Tacticals.New.tclTHENS (Proofview.V82.tactic (cut decide))
             [(Tacticals.New.tclTHEN  intro
              (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case)
                        (Proofview.V82.tactic clear_last)));
              decideEquality rectype])
+  end
 
 
 (* User syntax *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 782ca67d52..284199586a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -221,17 +221,18 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     | Some (tac, FirstSolved) -> true, true, Some (Tacticals.New.tclCOMPLETE tac)
     | Some (tac, AllMatches) -> true, false, Some (Tacticals.New.tclCOMPLETE tac)
   in
-  let cs =
-    Goal.env >- fun env ->
-    Goal.concl >- fun concl ->
-    Goal.V82.to_sensitive (
-      (if not all then instantiate_lemma else instantiate_lemma_all frzevars)
-        env ) >- fun instantiate_lemma ->
-      let typ =
-        match cls with None -> Goal.return concl | Some id -> Tacmach.New.pf_get_hyp_typ_sensitive id
-      in
-      typ >- fun typ ->
-      Goal.return (instantiate_lemma c t l l2r typ)
+  let cs gl =
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    let instantiate_lemma =
+      Tacmach.New.of_old 
+        ((if not all then instantiate_lemma else instantiate_lemma_all frzevars) env)
+        gl
+    in
+    let typ =
+      match cls with None -> concl | Some id -> Tacmach.New.pf_get_hyp_typ id gl
+    in
+    instantiate_lemma c t l l2r typ
   in
   let try_clause c =
     side_tac
@@ -240,11 +241,13 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
          (Proofview.V82.tactic (general_elim_clause with_evars frzevars cls c elim)))
       tac
   in
-    Proofview.Goal.lift cs >>= fun cs ->
+  Proofview.Goal.enter begin fun gl ->
+    let cs = cs gl in
     if firstonly then
       Tacticals.New.tclFIRST (List.map try_clause cs)
     else
       Tacticals.New.tclMAP try_clause cs
+  end
 
 (* The next function decides in particular whether to try a regular
   rewrite or a generalized rewrite.
@@ -325,18 +328,22 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 
 let type_of_clause = function
   | None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl))
-  | Some id -> Tacmach.New.pf_get_hyp_typ id
+  | Some id -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (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 dep = dep_proof_ok && dep_fun c type_of_cls in
-  Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) >>= fun (elim,effs) ->
+  let (elim,effs) =
+    Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) gl
+  in
   Proofview.V82.tactic (Tactics.emit_side_effects effs) <*>
   general_elim_clause with_evars frzevars tac cls c t l
     (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)}
+  end
 
 let adjust_rewriting_direction args lft2rgt =
   match args with
@@ -449,13 +456,14 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	in
 	let do_hyps =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
-	  let ids =
+	  let ids gl =
 	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
-              Tacmach.New.pf_ids_of_hyps_sensitive >- fun ids_of_hyps ->
-	      Goal.return (Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps)
+            let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
+	    Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
 	  in
-          Proofview.Goal.lift ids >>= fun ids ->
-          do_hyps_atleastonce ids
+          Proofview.Goal.enter begin fun gl ->
+            do_hyps_atleastonce (ids gl)
+          end
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
 	  Tacticals.New.tclIFTHENTRYELSEMUST
@@ -508,10 +516,11 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
       | None -> Proofview.tclUNIT ()
       | Some tac ->  Tacticals.New.tclCOMPLETE tac
   in
-  Tacmach.New.pf_apply get_type_of >>= fun get_type_of ->
+  Proofview.Goal.enter begin fun gl ->
+  let get_type_of = Tacmach.New.pf_apply get_type_of gl in
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
-  Tacmach.New.pf_apply is_conv >>= fun is_conv ->
+  let is_conv = Tacmach.New.pf_apply is_conv gl in
   if unsafe || (is_conv t1 t2) then
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
@@ -529,7 +538,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
       ]
   else
     Tacticals.New.tclFAIL 0 (str"Terms do not have convertible types.")
-
+  end
 
 let replace c2 c1 = multi_replace onConcl c2 c1 false None
 
@@ -794,12 +803,14 @@ let rec build_discriminator sigma env dirn c sort = function
 *)
 
 let gen_absurdity id =
-  Tacmach.New.pf_get_hyp_typ id >>= fun hyp_typ ->
+  Proofview.Goal.enter begin fun gl ->
+  let hyp_typ = Tacmach.New.pf_get_hyp_typ id gl in
   if is_empty_type hyp_typ
   then
     simplest_elim (mkVar id)
   else
     Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
+  end
 
 (* Precondition: eq is leibniz equality
 
@@ -860,28 +871,31 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
     | Inr _ ->
 	Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
     | Inl (cpath, (_,dirn), _) ->
-        Tacmach.New.pf_apply get_type_of >>= fun get_type_of ->
-	let sort = get_type_of concl in
+	let sort = Tacmach.New.pf_apply get_type_of gl concl in
 	discr_positions env sigma u eq_clause cpath dirn sort
   end
 
 let onEquality with_evars tac (c,lbindc) =
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+  Proofview.Goal.enter begin fun gl ->
+  let type_of = Tacmach.New.pf_apply Typing.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
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
-  Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) >>= fun eq_clause ->
+  let eq_clause = Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) gl in
   begin try (* clenv_pose_dependent_evars can raise exceptions *)
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
-  Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) >>= fun (eq,eq_args) ->
+  let (eq,eq_args) =
+    Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) gl
+  in
   Tacticals.New.tclTHEN
     (Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
     (tac (eq,eqn,eq_args) eq_clause')
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let onNegatedEquality with_evars tac =
   Proofview.Goal.enter begin fun gl ->
@@ -1278,7 +1292,9 @@ let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter begin fun gl ->
-    Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
+    let sort =
+      Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) gl
+    in
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma t1 t2 with
@@ -1572,7 +1588,7 @@ let subst_one_var dep_proof_ok x =
   Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
     let hyps = Environ.named_context_of_val hyps in
-    Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) ->
+    let (_,xval,_) = Tacmach.New.pf_get_hyp x gl in
     (* If x has a body, simply replace x with body and clear x *)
     if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else
       (* x is a variable: *)
@@ -1586,7 +1602,7 @@ let subst_one_var dep_proof_ok x =
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
         with FoundHyp res -> res in
-      Tacmach.New.of_old found >>= fun (hyp,rhs,dir) ->
+      let (hyp,rhs,dir) = Tacmach.New.of_old found gl in
       subst_one dep_proof_ok x (hyp,rhs,dir)
   end
 
@@ -1611,7 +1627,8 @@ let default_subst_tactic_flags () =
     { only_leibniz = true; rewrite_dependent_proof = false }
 
 let subst_all ?(flags=default_subst_tactic_flags ()) () =
-  Tacmach.New.of_old find_eq_data_decompose >>= fun find_eq_data_decompose ->
+  Proofview.Goal.enter begin fun gl ->
+  let find_eq_data_decompose = Tacmach.New.of_old find_eq_data_decompose gl in
   let test (_,c) =
     try
       let lbeq,(_,x,y) = find_eq_data_decompose c in
@@ -1623,10 +1640,11 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
     with PatternMatchingFailure -> failwith "caught"
   in
   let test p = try Some (test p) with Failure _ -> None in
-  Tacmach.New.pf_hyps_types >>= fun hyps ->
+  let hyps = Tacmach.New.pf_hyps_types gl in
   let ids = List.map_filter test hyps in
   let ids = List.uniquize ids in
   subst_gen flags.rewrite_dependent_proof ids
+  end
 
 (* Rewrite the first assumption for which the condition faildir does not fail
    and gives the direction of the rewrite *)
@@ -1679,6 +1697,9 @@ 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 fcb1311617..088ce71d46 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -644,10 +644,12 @@ END
 exception Found of unit Proofview.tactic
 
 let rewrite_except h =
-  Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+  Proofview.Goal.enter begin fun gl ->
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
   Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else 
       Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
     hyps
+  end
 
 
 let refl_equal = 
@@ -661,7 +663,8 @@ let refl_equal =
   should be replaced by a call to the tactic but I don't know how to
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
-      Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) >>= fun type_of_a ->
+  Proofview.Goal.enter begin fun gl ->
+    let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in
        Tacticals.New.tclTHENLIST
          [Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
           Proofview.Goal.enter begin fun gl ->
@@ -673,6 +676,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
             end
           end;
 	  simplest_case a]
+  end
 
 
 let case_eq_intros_rewrite x =
@@ -685,9 +689,9 @@ let case_eq_intros_rewrite x =
       mkCaseEq x;
     Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
-      Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+      let hyps = Tacmach.New.pf_ids_of_hyps gl in
       let n' = nb_prod concl in
-      Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>= fun h ->
+      let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in
       Tacticals.New.tclTHENLIST [
                     Tacticals.New.tclDO (n'-n-1) intro;
 		    Proofview.V82.tactic (Tacmach.introduction h);
@@ -713,10 +717,12 @@ let destauto t =
   with Found tac -> tac
 
 let destauto_in id = 
-  Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) >>= fun ctype ->
+  Proofview.Goal.enter begin fun gl ->
+  let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
+  end
 
 TACTIC EXTEND destauto
 | [ "destauto" ] -> [ Proofview.Goal.enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b3c8b2837e..ebccd95b7a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -274,11 +274,13 @@ Nota: with Inversion_clear, only four useless hypotheses
 *)
 
 let generalizeRewriteIntros tac depids id =
-  Tacmach.New.of_old (dependent_hyps id depids) >>= fun dids ->
+  Proofview.Goal.enter begin fun gl ->
+  let dids = Tacmach.New.of_old (dependent_hyps id depids) gl in
   (Tacticals.New.tclTHENLIST
     [Proofview.V82.tactic (bring_hyps dids); tac;
      (* may actually fail to replace if dependent in a previous eq *)
      intros_replacing (ids_of_named_context dids)])
+  end
 
 let rec tclMAP_i n tacfun = function
   | [] -> Tacticals.New.tclDO n (tacfun None)
@@ -302,11 +304,15 @@ let projectAndApply thin id eqname names depids =
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
-    Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) >>= fun (t,t1,t2) ->
+    Proofview.Goal.enter begin fun gl ->
+    let (t,t1,t2) =
+      Tacmach.New.of_old (fun gls -> Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id)) gl
+    in
     match (kind_of_term t1, kind_of_term t2) with
     | Var id1, _ -> generalizeRewriteIntros (Proofview.V82.tactic (subst_hyp true id)) depids id1
     | _, Var id2 -> generalizeRewriteIntros (Proofview.V82.tactic (subst_hyp false id)) depids id2
     | _ -> tac id
+    end
   in
   let deq_trailer id _ neqns =
     Tacticals.New.tclTHENLIST
@@ -331,7 +337,10 @@ let projectAndApply thin id eqname names depids =
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
 let rewrite_equations_gene othin neqns ba =
-  Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>= fun (depids,nodepids) ->
+  Proofview.Goal.enter begin fun gl ->
+  let (depids,nodepids) =
+    Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) gl
+  in
   let rewrite_eqns =
     match othin with
       | Some thin ->
@@ -361,6 +370,7 @@ let rewrite_equations_gene othin neqns ba =
                (tclORELSE (clear [id])
                  (tclTHEN (bring_hyps [d]) (clear [id]))))
        depids)])
+  end
 
 (* Introduction of the equations on arguments
    othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -397,8 +407,11 @@ let extract_eqn_names = function
   | Some x -> x
 
 let rewrite_equations othin neqns names ba =
+  Proofview.Goal.enter begin fun gl ->
   let names = List.map (get_names true) names in
-  Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) >>= fun (depids,nodepids) ->
+  let (depids,nodepids) =
+    Tacmach.New.of_old (fun gl -> split_dep_and_nodep ba.assums gl) gl
+  in
   let rewrite_eqns =
     let first_eq = ref MoveLast in
     match othin with
@@ -424,6 +437,7 @@ let rewrite_equations othin neqns names ba =
      Proofview.V82.tactic (bring_hyps nodepids);
      Proofview.V82.tactic (clear (ids_of_named_context nodepids));
      rewrite_eqns])
+  end
 
 let interp_inversion_kind = function
   | SimpleInversion -> None
@@ -448,8 +462,8 @@ let raw_inversion inv_kind id status names =
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
-    Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind ->
-    Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+    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
     begin
       try
         Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
@@ -457,7 +471,7 @@ let raw_inversion inv_kind id status names =
         Proofview.tclZERO (Errors.UserError ("raw_inversion" ,
 	                                     str ("The type of "^(Id.to_string id)^" is not inductive.")))
     end >= fun (ind,t) ->
-      Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
+      let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) gl in
       let ccl = clenv_type indclause in
       check_no_metas indclause ccl;
       let IndType (indf,realargs) = find_rectype env sigma ccl in
@@ -526,7 +540,7 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
 
 let invIn k names ids id =
   Proofview.Goal.enter begin fun gl ->
-    Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+    let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in
     let concl = Proofview.Goal.concl gl in
     let nb_prod_init = nb_prod concl in
     let intros_replace_ids =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e726e76921..86ec3a8357 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -285,7 +285,7 @@ let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv i
 
 let lemInvIn id c ids =
   Proofview.Goal.enter begin fun gl ->
-    Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+    let hyps = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) ids in
     let intros_replace_ids =
       let concl = Proofview.Goal.concl gl in
       let nb_of_new_hyp  = nb_prod concl - List.length ids in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 14a9eb0ed6..f40ec76595 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1820,7 +1820,8 @@ let setoid_transitivity c =
     (transitivity_red true c)
 
 let setoid_symmetry_in id =
-  Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) >>= fun ctype ->
+  Proofview.Goal.enter begin fun gl ->
+  let ctype = Tacmach.New.of_old (fun gl -> pf_type_of gl (mkVar id)) gl in
   let binders,concl = decompose_prod_assum ctype in
   let (equiv, args) = decompose_app concl in
   let rec split_last_two = function
@@ -1835,6 +1836,7 @@ let setoid_symmetry_in id =
     Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp))
       [ Proofview.V82.tactic (intro_replacing id);
 	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic (Tactics.assumption) ] ]
+  end
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 83958eca28..2bf3c8e065 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1179,9 +1179,11 @@ and interp_ltac_reference loc' mustbetac ist = function
 
 and interp_tacarg ist arg =
   let tac_of_old f =
-    Tacmach.New.of_old f >>== fun (sigma,v) ->
-    Proofview.V82.tclEVARS sigma <*>
-    (Proofview.Goal.return v)
+    Proofview.Goal.enterl begin fun gl ->
+      let (sigma,v) = Tacmach.New.of_old f gl in
+      Proofview.V82.tclEVARS sigma <*>
+      (Proofview.Goal.return v)
+    end
   in
   match arg with
   | TacGeneric arg ->
@@ -1209,8 +1211,10 @@ and interp_tacarg ist arg =
       end la ((Proofview.Goal.return [])) >>== fun la_interp ->
       tac_of_old (fun gl -> interp_external loc ist { gl with sigma=project gl } com req la_interp)
   | TacFreshId l ->
-      Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) >>== fun id ->
+      Proofview.Goal.enterl begin fun gl ->
+      let id = Tacmach.New.of_old (fun gl -> pf_interp_fresh_id ist gl l) gl in
       (Proofview.Goal.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)))
+      end
   | Tacexp t -> val_interp ist t
   | TacDynamic(_,t) ->
       let tg = (Dyn.tag t) in
@@ -1465,8 +1469,8 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
             end
         in
         let init_match_pattern = Tacmach.New.of_old (fun gl ->
-          apply_one_mhyp_context gl lmatch hyp_pat lhyps_rest) in
-        init_match_pattern >>== match_next_pattern
+          apply_one_mhyp_context gl lmatch hyp_pat lhyps_rest) gl in
+        match_next_pattern init_match_pattern
     | [] ->
         let lfun = lfun +++ ist.lfun in
         let lfun = extend_values_with_bindings lmatch lfun in
@@ -1712,8 +1716,12 @@ and interp_atomic ist tac =
   match tac with
   (* Basic tactics *)
   | TacIntroPattern l ->
-      Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) >>= fun patterns ->
+      Proofview.Goal.enter begin fun gl ->
+      let patterns =
+        Tacmach.New.of_old (fun gl -> interp_intro_pattern_list_as_list ist gl l) gl
+      in
       h_intro_patterns patterns
+      end
   | TacIntrosUntil hyp ->
       begin try (* interp_quantified_hypothesis can raise an exception *)
         h_intros_until (interp_quantified_hypothesis ist hyp)
@@ -1722,7 +1730,7 @@ and interp_atomic ist tac =
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-        Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
+        let mloc = Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) gl in
         h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
       end
   | TacAssumption -> Proofview.V82.tactic h_assumption
@@ -1762,8 +1770,10 @@ and interp_atomic ist tac =
             | None -> fun l -> Proofview.V82.tactic (h_apply a ev l)
             | Some cl ->
                 (fun l ->
-                  Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) >>= fun cl ->
-                  h_apply_in a ev l cl) in
+                  Proofview.Goal.enter begin fun gl ->
+                  let cl = Tacmach.New.of_old (fun gl -> interp_in_hyp_as ist gl cl) gl in
+                  h_apply_in a ev l cl
+                  end) in
           Tacticals.New.tclWITHHOLES ev tac sigma l
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
@@ -1858,7 +1868,7 @@ and interp_atomic ist tac =
         let sigma = Proofview.Goal.sigma gl in
         try (* intrerpreation function may raise exceptions *)
           let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
-          Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
+          let patt = Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) gl in
           Tacticals.New.tclTHEN
 	    (Proofview.V82.tclEVARS sigma)
             (Tactics.forward (Option.map (interp_tactic ist) t)
@@ -1884,11 +1894,15 @@ and interp_atomic ist tac =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>= fun clp ->
-        Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>= fun eqpat ->
+        let clp = Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) gl in
+        let eqpat =
+          Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) gl
+        in
         if Locusops.is_nowhere clp then
         (* We try to fully-typecheck the term *)
-          Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+          let (sigma,c_interp) =
+            Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
+          in
 	Tacticals.New.tclTHEN
 	  (Proofview.V82.tclEVARS sigma)
           (h_let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
@@ -1926,21 +1940,20 @@ and interp_atomic ist tac =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let l =
-          Goal.sensitive_list_map begin fun (c,(ipato,ipats)) ->
-            Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c ->
-              Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern ->
-                Goal.return begin
-                  c,
-                  (Option.map interp_intro_pattern ipato,
-                   Option.map interp_intro_pattern ipats)
-                end
+          List.map begin fun (c,(ipato,ipats)) ->
+            let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in
+            let interp_intro_pattern =
+              Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) gl
+            in
+            c,
+            (Option.map interp_intro_pattern ipato,
+             Option.map interp_intro_pattern ipats)
           end l
         in
         let sigma = Proofview.Goal.sigma gl in
-        Proofview.Goal.lift l >>= fun l ->
         let sigma,el =
           Option.fold_map (interp_constr_with_bindings ist env) sigma el in
-        Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>= fun interp_clause ->
+        let interp_clause = Tacmach.New.of_old (fun gl -> interp_clause ist gl) gl in
         let cls = Option.map interp_clause cls in
         Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
       end
@@ -1949,21 +1962,27 @@ and interp_atomic ist tac =
       let h2 = interp_quantified_hypothesis ist h2 in
       Elim.h_double_induction h1 h2
   | TacDecomposeAnd c ->
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+      Proofview.Goal.enter begin fun gl ->
+      let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
       Tacticals.New.tclTHEN
 	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose_and c_interp)
+      end
   | TacDecomposeOr c ->
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+      Proofview.Goal.enter begin fun gl ->
+      let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
       Tacticals.New.tclTHEN
 	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose_or c_interp)
+      end
   | TacDecompose (l,c) ->
+      Proofview.Goal.enter begin fun gl ->
       let l = List.map (interp_inductive ist) l in
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+      let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
       Tacticals.New.tclTHEN
 	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose l c_interp)
+      end
   | TacSpecialize (n,cb) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
@@ -2095,71 +2114,94 @@ and interp_atomic ist tac =
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
   | TacSymmetry c ->
-      Tacmach.New.of_old (fun gl -> interp_clause ist gl c) >>= fun cl ->
+      Proofview.Goal.enter begin fun gl ->
+      let cl = Tacmach.New.of_old (fun gl -> interp_clause ist gl c) gl in
       h_symmetry cl
+      end
   | TacTransitivity c ->
       begin match c with
       | None -> h_transitivity None
       | Some c ->
-          Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
+          Proofview.Goal.enter begin fun gl ->
+          let (sigma,c_interp) =
+            Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
+          in
           Tacticals.New.tclTHEN
 	    (Proofview.V82.tclEVARS sigma)
 	    (h_transitivity (Some c_interp))
+          end
       end
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
+      Proofview.Goal.enter begin fun gl ->
       let l = List.map (fun (b,m,c) ->
         let f env sigma = interp_open_constr_with_bindings ist env sigma c in
 	(b,m,f)) l in
-      Tacmach.New.of_old (fun gl -> interp_clause ist gl cl) >>= fun cl ->
+      let cl = Tacmach.New.of_old (fun gl -> interp_clause ist gl cl) gl in
       Equality.general_multi_multi_rewrite ev l cl
         (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)
+      end
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Proofview.tclEVARMAP >= fun sigma ->
-      Proofview.Goal.lift begin match c with
-      | None -> Goal.return (sigma , None)
-      | Some c ->
-          Goal.V82.to_sensitive (fun gl -> pf_interp_constr ist gl c) >- fun (sigma,c_interp) ->
-	  Goal.return (sigma , Some c_interp)
-      end >>= fun (sigma,c_interp) ->
-      Tacmach.New.of_old (interp_intro_pattern ist) >>= fun interp_intro_pattern ->
-      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>= fun dqhyps ->
+      Proofview.Goal.enter begin fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
+      let (sigma,c_interp) =
+        match c with
+        | None -> sigma , None
+        | Some c ->
+            let (sigma,c_interp) =
+              Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl
+            in
+            sigma , Some c_interp
+      in
+      let interp_intro_pattern = Tacmach.New.of_old (interp_intro_pattern ist) gl in
+      let dqhyps =
+        Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) gl
+      in
       Inv.dinv k c_interp
         (Option.map interp_intro_pattern ids)
         dqhyps
+      end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
-      Tacmach.New.of_old (interp_intro_pattern ist) >>= fun interp_intro_pattern ->
-      Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>= fun hyps ->
-      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>= fun dqhyps ->
+      Proofview.Goal.enter begin fun gl ->
+      let interp_intro_pattern = Tacmach.New.of_old (interp_intro_pattern ist) gl in
+      let hyps = Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) gl in
+      let dqhyps = Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) gl in
       Inv.inv_clause k
         (Option.map interp_intro_pattern ids)
         hyps
         dqhyps
+      end
   | TacInversion (InversionUsing (c,idl),hyp) ->
-      Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) >>= fun (sigma,c_interp) ->
-      Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) >>= fun dqhyps ->
-      Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) >>= fun hyps ->
+      Proofview.Goal.enter begin fun gl ->
+      let (sigma,c_interp) = Tacmach.New.of_old (fun gl -> pf_interp_constr ist gl c) gl in
+      let dqhyps = Tacmach.New.of_old (fun gl -> interp_declared_or_quantified_hypothesis ist gl hyp) gl in
+      let hyps = Tacmach.New.of_old (fun gl -> interp_hyp_list ist gl idl) gl in
       Leminv.lemInv_clause dqhyps
         c_interp
         hyps
+      end
 
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
-      Proofview.tclEVARMAP >= fun goal_sigma ->
+      Proofview.Goal.enter begin fun gl ->
+      let goal_sigma = Proofview.Goal.sigma gl in
       let tac = lookup_tactic opn in
-      Tacmach.New.of_old begin fun gl ->
+      let (sigma,args) = Tacmach.New.of_old begin fun gl ->
 	List.fold_right begin fun a (sigma,acc) ->
 	  let (sigma,a_interp) = interp_genarg ist { gl with sigma=sigma } a in
 	  sigma , a_interp::acc
 	end l (goal_sigma,[])
-      end >>= fun (sigma,args) ->
+      end gl in
       Proofview.V82.tclEVARS sigma <*>
       tac args ist
+      end
   | TacAlias (loc,s,l,(_,body)) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
-      let rec f x = match genarg_tag x with
+      let rec f x =
+        Proofview.Goal.enterl begin fun gl ->
+        match genarg_tag x with
           | IntOrVarArgType ->
               (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
           | IdentArgType b ->
@@ -2168,40 +2210,49 @@ and interp_atomic ist tac =
 	                                       (out_gen (glbwit (wit_ident_gen b)) x)))
               end
           | VarArgType ->
-              Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x))
+              Proofview.Goal.return (
+                Tacmach.New.of_old (fun gl -> mk_hyp_value ist gl (out_gen (glbwit wit_var) x))
+                  gl
+              )
           | RefArgType ->
+              Proofview.Goal.return (
               Tacmach.New.of_old (fun gl -> 
                 Value.of_constr (constr_of_global
                                    (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))))
+                gl
+              )
           | GenArgType -> f (out_gen (glbwit wit_genarg) x)
           | ConstrArgType ->
-              Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) >>== fun (sigma,v) ->
+              Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_constr_value ist gl (out_gen (glbwit wit_constr) x)) gl) >>== fun (sigma,v) ->
               (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | OpenConstrArgType false ->
-              Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) >>== fun (sigma,v) ->
+              Proofview.Goal.return (
+                Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl) >>== fun (sigma,v) ->
               (Proofview.V82.tclEVARS sigma) <*>
 	      (Proofview.Goal.return v)
           | ConstrMayEvalArgType ->
-              Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x)) >>== fun (sigma,c_interp) ->
+              Proofview.Goal.return (
+                Tacmach.New.of_old (fun gl -> interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x))
+                   gl) >>== fun (sigma,c_interp) ->
               Proofview.V82.tclEVARS sigma <*>
 	      Proofview.Goal.return (Value.of_constr c_interp)
           | ListArgType ConstrArgType ->
               let wit = glbwit (wit_list wit_constr) in
-              Tacmach.New.of_old begin fun gl ->
+              let (sigma,l_interp) = Tacmach.New.of_old begin fun gl ->
 	        List.fold_right begin fun c (sigma,acc) ->
 	          let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
 	          sigma , c_interp::acc
 	        end (out_gen wit x) (project gl,[])
-              end >>== fun (sigma,l_interp) ->
+              end gl in
               (Proofview.V82.tclEVARS sigma) <*>
               (Proofview.Goal.return (in_gen (topwit (wit_list wit_genarg)) l_interp))
           | ListArgType VarArgType ->
               let wit = glbwit (wit_list wit_var) in
-              Tacmach.New.of_old (fun gl ->
+              Proofview.Goal.return (Tacmach.New.of_old (fun gl ->
                 let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
                 in_gen (topwit (wit_list wit_genarg)) ans
-              )
+              ) gl)
           | ListArgType IntOrVarArgType ->
               let wit = glbwit (wit_list wit_int_or_var) in
               let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
@@ -2228,8 +2279,8 @@ and interp_atomic ist tac =
                 val_interp ist tac >>== fun v ->
                 Proofview.Goal.return v
               else
-                Tacmach.New.of_old (fun gl ->
-                  Geninterp.generic_interp ist gl x) >>== fun (newsigma,v) ->
+                let (newsigma,v) = Tacmach.New.of_old (fun gl ->
+                  Geninterp.generic_interp ist gl x) gl in
                 Proofview.V82.tactic (tclEVARS newsigma) <*>
                 Proofview.Goal.return v
           | QuantHypArgType | RedExprArgType
@@ -2237,6 +2288,7 @@ and interp_atomic ist tac =
           | BindingsArgType
           | OptArgType _ | PairArgType _
 	    -> Proofview.tclZERO (UserError("" , str"This argument type is not supported in tactic notations."))
+        end
       in
       let addvar (x, v) accu =
         accu >>== fun accu ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5d3c8b97ab..265af5b08f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -554,38 +554,47 @@ module New = struct
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Tacmach.New.pf_get_hyp_typ id >>= fun typ ->
+    Proofview.Goal.enter begin fun gl ->
+    let typ = Tacmach.New.pf_get_hyp_typ id gl in
     if pred (id,typ) then
       tac1 id
     else
       tac2 id
+    end
 
   let fullGoal =
-    Tacmach.New.pf_ids_of_hyps >>== fun hyps ->
+    Proofview.Goal.enterl begin fun gl ->
+    let hyps = Tacmach.New.pf_ids_of_hyps gl in
     Proofview.Goal.return (None :: List.map Option.make hyps)
+    end
 
   let tryAllHyps tac =
-    Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+    Proofview.Goal.enter begin fun gl ->
+    let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclFIRST_PROGRESS_ON tac hyps
+    end
   let tryAllHypsAndConcl tac =
     fullGoal >>= fun fullGoal ->
     tclFIRST_PROGRESS_ON tac fullGoal
 
   let onClause tac cl =
-    Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
+    Proofview.Goal.enter begin fun gl ->
+    let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
+    end
 
   (* Find the right elimination suffix corresponding to the sort of the goal *)
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
       isrec allnames tac predicate (indbindings,elimbindings)
       ind indclause =
-    Tacmach.New.of_old (mk_elim ind) >>= fun elim ->
+    Proofview.Goal.enter begin fun gl ->
+    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
-    Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+    let type_of = Tacmach.New.pf_apply Typing.type_of gl in
     begin try (* type_of can raise an exception *)
-            Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim))
+            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 indmv =
@@ -634,10 +643,14 @@ module New = struct
             Reduction.CONV (mkMeta pmv) p elimclause'
     in
     new_elim_res_pf_THEN_i elimclause' branchtacs
+    end
 
   let elimination_then_using tac predicate bindings c =
-    Tacmach.New.of_old (fun gl -> pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>= fun (ind,t) ->
-    Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
+    Proofview.Goal.enter begin fun gl ->
+    let (ind,t) =
+      Tacmach.New.of_old (fun gl -> pf_reduce_to_quantified_ind gl (pf_type_of gl c)) gl
+    in
+    let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) gl in
     let isrec,mkelim =
       if (Global.lookup_mind (fst ind)).mind_record
       then false,gl_make_case_dep
@@ -645,6 +658,7 @@ module New = struct
     in
     general_elim_then_using mkelim isrec
       None tac predicate bindings ind indclause
+    end
 
   let case_then_using =
     general_elim_then_using gl_make_case_dep false
@@ -656,10 +670,14 @@ module New = struct
   let elimination_then tac        = elimination_then_using tac None
 
   let elim_on_ba tac ba =
-    Tacmach.New.of_old (make_elim_branch_assumptions ba) >>= fun branches ->
+    Proofview.Goal.enter begin fun gl ->
+    let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
     tac branches
+    end
 
   let case_on_ba tac ba = 
-    Tacmach.New.of_old (make_case_branch_assumptions ba) >>= fun branches ->
+    Proofview.Goal.enter begin fun gl ->
+    let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
     tac branches
+    end
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5e62451f9a..c317ca0d44 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -606,8 +606,10 @@ let depth_of_quantified_hypothesis red h gl =
 	  str".")
 
 let intros_until_gen red h =
-  Tacmach.New.of_old (depth_of_quantified_hypothesis red h) >>= fun n ->
+  Proofview.Goal.enter begin fun gl ->
+  let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in
   Tacticals.New.tclDO n (if red then introf else intro)
+  end
 
 let intros_until_id id = intros_until_gen true (NamedHyp id)
 let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
@@ -873,8 +875,10 @@ let find_eliminator c gl =
 
 let default_elim with_evars (c,_ as cx) =
   Proofview.tclORELSE
-    (Tacmach.New.of_old (find_eliminator c) >>= fun elim ->
-     Proofview.V82.tactic (general_elim with_evars cx elim))
+    (Proofview.Goal.enter begin fun gl ->
+      let elim = Tacmach.New.of_old (find_eliminator c) gl in
+      Proofview.V82.tactic (general_elim with_evars cx elim)
+    end)
     begin function
       | IsRecord ->
           (* For records, induction principles aren't there by default
@@ -1285,7 +1289,9 @@ let check_number_of_constructors expctdnumopt i nconstr =
 let constructor_tac with_evars expctdnumopt i lbind =
   Proofview.Goal.enter begin fun gl ->
     let cl = Proofview.Goal.concl gl in
-    Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+    let reduce_to_quantified_ind =
+      Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
+    in
     try (* reduce_to_quantified_ind can raise an exception *)
       let (mind,redcl) = reduce_to_quantified_ind cl in
       let nconstr =
@@ -1309,7 +1315,9 @@ let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
   Proofview.Goal.enter begin fun gl ->
     let cl = Proofview.Goal.concl gl in
-    Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+    let reduce_to_quantified_ind =
+      Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
+    in
   try (* reduce_to_quantified_ind can raise an exception *)
     let mind = fst (reduce_to_quantified_ind cl) in
     let nconstr =
@@ -1386,9 +1394,12 @@ let intro_decomp_eq loc b l l' thin tac id gl =
     (eq,t,eq_args) eq_clause) gl
 
 let intro_or_and_pattern loc b ll l' thin tac id =
+  Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
-  Tacmach.New.of_old (fun gl ->
-    pf_reduce_to_quantified_ind gl (pf_type_of gl c)) >>= fun (ind,t) ->
+  let (ind,t) =
+    Tacmach.New.of_old (fun gl ->
+      pf_reduce_to_quantified_ind gl (pf_type_of gl c)) gl
+  in
   let nv = mis_constr_nargs ind in
   let bracketed = b || not (List.is_empty l') in
   let adjust n l = if bracketed then adjust_intro_patterns n l else l in
@@ -1398,6 +1409,7 @@ let intro_or_and_pattern loc b ll l' thin tac id =
     (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
     (Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
        nv (Array.of_list ll))
+  end
 
 let rewrite_hyp l2r id =
   let rew_on l2r =
@@ -1408,8 +1420,8 @@ 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
-    Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-    Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
+    let type_of = Tacmach.New.pf_apply Typing.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
       (* TODO: detect setoid equality? better detect the different equalities *)
@@ -1518,41 +1530,32 @@ let intro_patterns = function
 
 let make_id s = fresh_id [] (default_id_of_sort s)
 
-let prepare_intros s ipat =
-  let make_id s = Tacmach.New.of_old (make_id s) in
-  let fresh_id l id = Tacmach.New.of_old (fresh_id l id) in
-  let (>>=) t k =
-    t >>== fun x ->
-    Proofview.Goal.return (k x)
-  in
+let prepare_intros s ipat gl =
+  let make_id s = Tacmach.New.of_old (make_id s) gl in
+  let fresh_id l id = Tacmach.New.of_old (fresh_id l id) gl in
   match ipat with
   | None ->
-      make_id s >>= fun id ->
-      id , Proofview.tclUNIT ()
+      make_id s , Proofview.tclUNIT ()
   | Some (loc,ipat) -> match ipat with
   | IntroIdentifier id ->
-      Proofview.Goal.return (id, Proofview.tclUNIT ())
+      id, Proofview.tclUNIT ()
   | IntroAnonymous ->
-      make_id s >>= fun id ->
-      id  , Proofview.tclUNIT ()
+      make_id s  , Proofview.tclUNIT ()
   | IntroFresh id ->
-      fresh_id [] id >>= fun id ->
-      id , Proofview.tclUNIT ()
+      fresh_id [] id , Proofview.tclUNIT ()
   | IntroWildcard ->
-      make_id s >>= fun id ->
+      let id = make_id s in
       id , Proofview.V82.tactic (clear_wildcards [dloc,id])
   | IntroRewrite l2r ->
-      make_id s >>= fun id ->
-      id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+      let id = make_id s in
+      id , Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | IntroOrAndPattern ll ->
-      make_id s >>= fun id ->
-      id ,
+      make_id s ,
       Tacticals.New.onLastHypId
 	(intro_or_and_pattern loc true ll [] []
 	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
   | IntroInjection l ->
-      make_id s >>= fun id ->
-      id ,
+      make_id s ,
       Proofview.V82.tactic (onLastHypId
 	(intro_decomp_eq loc true l [] []
 	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
@@ -1577,15 +1580,17 @@ let clear_if_overwritten c ipats =
   | _ -> tclIDTAC
 
 let assert_as first ipat c =
-  Tacmach.New.of_old pf_hnf_type_of >>= fun hnf_type_of ->
+  Proofview.Goal.enter begin fun gl ->
+  let hnf_type_of = Tacmach.New.of_old pf_hnf_type_of gl in
   match kind_of_term (hnf_type_of c) with
   | Sort s ->
-      prepare_intros s ipat >>= fun (id,tac) ->
+      let (id,tac) = prepare_intros s ipat gl in
       let repl = not (Option.is_empty (allow_replace c ipat)) in
       Tacticals.New.tclTHENS
 	(Proofview.V82.tactic ((if first then internal_cut_gen else internal_cut_rev_gen) repl id c))
 	(if first then [Proofview.tclUNIT (); tac] else [tac; Proofview.tclUNIT ()])
   | _  -> Proofview.tclZERO (Errors.UserError ("",str"Not a proposition or a type."))
+  end
 
 let assert_tac na = assert_as true (ipat_of_name na)
 
@@ -1908,36 +1913,33 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
     let id =
       let t = match ty with Some t -> t | None -> typ_of env sigmac c in
       let x = id_of_name_using_hdchar (Global.env()) t name in
-      if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else
-        Proofview.Goal.lift begin
-          if not (mem_named_context x hyps) then Goal.return x else
+      if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else
+          if not (mem_named_context x hyps) then x else
 	    error ("The variable "^(Id.to_string x)^" is already declared.")
-        end in
-    id >>= fun id ->
-    Tacmach.New.of_old (letin_abstract id c test occs) >>= fun (depdecls,lastlhyp,ccl,c) ->
-    let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in
-    t >>= fun t ->
-    let newcl = match with_eq with
+    in
+    let (depdecls,lastlhyp,ccl,c) =
+      Tacmach.New.of_old (letin_abstract id c test occs) gl
+    in
+    let t =
+      match ty with Some t -> t | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) gl
+    in
+    let (newcl,eq_tac) = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
-            | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id))
-	    | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base)
-            | IntroIdentifier id -> (Proofview.Goal.return id)
-	    | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in
-          heq >>== fun heq ->
+            | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id)) gl
+	    | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base) gl
+            | IntroIdentifier id -> id
+	    | _ -> Errors.error "Expect an introduction pattern naming one hypothesis." in
             let eqdata = build_coq_eq_data () in
             let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
             let eq = applist (eqdata.eq,args) in
             let refl = applist (eqdata.refl, [t;mkVar id]) in
-            Proofview.Goal.return begin
               mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
               Tacticals.New.tclTHEN
 	        (intro_gen loc (IntroMustBe heq) lastlhyp true false)
 	        (Proofview.V82.tactic (thin_body [heq;id]))
-            end
       | None ->
-	  (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in
-    newcl >>= fun (newcl,eq_tac) ->
+	  (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
     Tacticals.New.tclTHENLIST
       [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
         intro_gen dloc (IntroMustBe id) lastlhyp true false;
@@ -1964,12 +1966,14 @@ let letin_pat_tac with_eq name c ty occs =
 let forward usetac ipat c =
   match usetac with
   | None ->
-      Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+      Proofview.Goal.enter begin fun gl ->
+      let type_of = Tacmach.New.pf_apply Typing.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))
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
+      end
   | Some tac ->
       Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac
 
@@ -2121,30 +2125,36 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
     match ra with
     | (RecArg,deprec,recvarname) ::
         (IndArg,depind,hyprecname) :: ra' ->
-        let recpat = match names with
+        Proofview.Goal.enter begin fun gl ->
+        let (recpat,names) = match names with
           | [loc,IntroIdentifier id as pat] ->
               let id' = next_ident_away (add_prefix "IH" id) avoid in
-	      (Proofview.Goal.return (pat, [dloc, IntroIdentifier id']))
-          | _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) in
-        recpat >>= fun (recpat,names) ->
+	      (pat, [dloc, IntroIdentifier id'])
+          | _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) gl in
         let dest = get_recarg_dest dests in
         safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin ->
-        let hyprec = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname depind gl names) in
-        hyprec >>= fun (hyprec,names) ->
-	safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
-	peel_tac ra' (update_dest dests ids') names thin))
+        Proofview.Goal.enter begin fun gl ->
+          let (hyprec,names) =
+            Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname depind gl names) gl
+          in
+	  safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
+	    peel_tac ra' (update_dest dests ids') names thin)
+        end)
+        end
     | (IndArg,dep,hyprecname) :: ra' ->
+        Proofview.Goal.enter begin fun gl ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
-        let pat = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname dep gl names) in
-        pat >>= fun (pat,names) ->
+        let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname dep gl names) gl in
 	safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
+        end
     | (RecArg,dep,recvarname) :: ra' ->
-        let pat = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) in
-        pat >>= fun (pat,names) ->
+        Proofview.Goal.enter begin fun gl ->
+        let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) gl in
         let dest = get_recarg_dest dests in
 	safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
+        end
     | (OtherArg,_,_) :: ra' ->
         let pat,names = match names with
           | [] -> (dloc, IntroAnonymous), []
@@ -2165,8 +2175,9 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 (* Marche pas... faut prendre en compte l'occurrence précise... *)
 
 let atomize_param_of_ind (indref,nparams,_) hyp0 =
-  Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
-  Tacmach.New.pf_apply reduce_to_quantified_ref >>= fun reduce_to_quantified_ref ->
+  Proofview.Goal.enter begin fun gl ->
+  let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
+  let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
   try (* reduce_to_quantified_ref can raise an exception *)
   let typ0 =  reduce_to_quantified_ref indref tmptyp0 in
   let prods, indtyp = decompose_prod typ0 in
@@ -2176,10 +2187,12 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   let rec atomize_one i avoid =
     Proofview.Goal.enter begin fun gl ->
     if not (Int.equal i nparams) then
-      Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
+      let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
       (* If argl <> [], we expect typ0 not to be quantified, in order to
          avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
-      Tacmach.New.pf_apply reduce_to_atomic_ref >>= fun reduce_to_atomic_ref ->
+      let reduce_to_atomic_ref =
+        Tacmach.New.pf_apply reduce_to_atomic_ref gl
+      in
       let indtyp = reduce_to_atomic_ref indref tmptyp0 in
       let argl = snd (decompose_app indtyp) in
       let c = List.nth argl (i-1) in
@@ -2188,15 +2201,15 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
 	| Var id when not (List.exists (occur_var env id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid)
 	| Var id ->
-            Tacmach.New.of_old (fresh_id [] id) >>= fun x ->
+            let x = Tacmach.New.of_old (fresh_id [] id) gl in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
 	| _ ->
-            Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+            let type_of = Tacmach.New.pf_apply Typing.type_of gl in
 	    let id = id_of_name_using_hdchar (Global.env()) (type_of c)
 		       Anonymous in
-            Tacmach.New.of_old (fresh_id [] id) >>= fun x ->
+            let x = Tacmach.New.of_old (fresh_id [] id) gl in
 	    Tacticals.New.tclTHEN
 	      (letin_tac None (Name x) c None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid))
@@ -2206,6 +2219,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   in
   atomize_one (List.length argl) params
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let find_atomic_param_of_ind nparams indtyp =
   let argl = snd (decompose_app indtyp) in
@@ -2663,25 +2677,22 @@ let abstract_args gl generalize_vars dep id defined f args =
     else None
 
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
-  Proofview.tclUNIT () >= fun () -> (* delay for [check_required_library] *)
+  Proofview.Goal.enter begin fun gl ->
   Coqlib.check_required_library Coqlib.jmeq_module_name;
-  let args = 
-    Tacmach.New.pf_get_new_id id >>== fun oldid ->
-    Tacmach.New.pf_get_hyp id >>== fun (_, b, t) ->
-    Proofview.Goal.return begin
+  let (f, args, def, id, oldid) =
+    let oldid = Tacmach.New.pf_get_new_id id gl in
+    let (_, b, t) = Tacmach.New.pf_get_hyp id gl in
       match b with
       | None -> let f, args = decompose_app t in
 	        (f, args, false, id, oldid)
       | Some t -> 
 	  let f, args = decompose_app t in
 	  (f, args, true, id, oldid)
-    end
   in
-  args >>= fun (f, args, def, id, oldid) ->
   if List.is_empty args then Proofview.tclUNIT ()
   else 
     let args = Array.of_list args in
-    Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) >>= fun newc ->
+    let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
       match newc with
       | None -> Proofview.tclUNIT ()
       | Some (newc, dep, n, vars) -> 
@@ -2697,6 +2708,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
               (Proofview.V82.tactic (fun gl -> tclFIRST [revert vars ;
 				   tclMAP (fun id -> 
 				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl))
+  end
 
 let rec compare_upto_variables x y =
   if (isVar x || isRel x) && (isVar y || isRel y) then true
@@ -3123,13 +3135,15 @@ let induction_tac_felim with_evars indvars nparams elim gl =
    induction applies with the induction hypotheses *)
 
 let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names tac =
-  Tacmach.New.of_old (get_eliminator elim) >>= fun (isrec, elim, indsign) ->
+  Proofview.Goal.enter begin fun gl ->
+  let (isrec, elim, indsign) = Tacmach.New.of_old (get_eliminator elim) gl in
   let names = compute_induction_names (Array.length indsign) names in
   (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
     (Tacticals.New.tclTHEN
        (induct_tac elim)
        (Proofview.V82.tactic (tclMAP (fun id -> tclTRY (expand_hyp id)) (List.rev indhyps))))
     (Array.map2 (induct_discharge destopt avoid tac) indsign names)
+  end
 
 (* Apply induction "in place" taking into account dependent
    hypotheses from the context *)
@@ -3218,8 +3232,11 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
 
 let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps =
-  Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
-  Tacmach.New.pf_apply reduce_to_quantified_ref >>= fun reduce_to_quantified_ref ->
+  Proofview.Goal.enter begin fun gl ->
+  let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
+  let reduce_to_quantified_ref =
+    Tacmach.New.pf_apply reduce_to_quantified_ref gl
+  in
   try (* reduce_to_quantified_ref can raise an exception *)
   let typ0 = reduce_to_quantified_ref indref tmptyp0 in
   let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in
@@ -3231,19 +3248,23 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   apply_induction_in_context
     (Some (hyp0,inhyps)) elim indvars names induct_tac
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
-  Tacmach.New.of_old (find_induction_type isrec elim hyp0) >>= fun elim_info ->
+  Proofview.Goal.enter begin fun gl ->
+  let elim_info = Tacmach.New.of_old (find_induction_type isrec elim hyp0) gl in
   Tacticals.New.tclTHEN
     (atomize_param_of_ind elim_info hyp0)
     (induction_from_context isrec with_evars elim_info
       (hyp0,lbind) names inhyps)
+  end
 
 (* Induction on a list of induction arguments. Analyse the elim
    scheme (which is mandatory for multiple ind args), check that all
    parameters and arguments are given (mandatory too). *)
 let induction_without_atomization isrec with_evars elim names lid =
-  Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) >>= fun (indsign,scheme as elim_info) ->
+  Proofview.Goal.enter begin fun gl ->
+  let (indsign,scheme as elim_info) = Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) gl in
   let awaited_nargs =
     scheme.nparams + scheme.nargs
     + (if scheme.farg_in_concl then 1 else 0)
@@ -3253,6 +3274,7 @@ let induction_without_atomization isrec with_evars elim names lid =
   if not (Int.equal nlid awaited_nargs)
   then Proofview.tclZERO (Errors.UserError ("", str"Not the right number of induction arguments."))
   else induction_from_context_l with_evars elim_info lid names
+  end
 
 let has_selected_occurrences = function
   | None -> false
@@ -3301,7 +3323,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
           let env = Proofview.Goal.env gl in
 	  let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
 	        Anonymous in
-          Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
+          let id = Tacmach.New.of_old (fresh_id [] x) gl in
 	(* We need the equality name now *)
 	  let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
@@ -3339,19 +3361,21 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 		atomize_list l'
 
 	    | _ ->
-                Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+                Proofview.Goal.enter begin fun gl ->
+                let type_of = Tacmach.New.pf_apply Typing.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
 
-                Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
+                let id = Tacmach.New.of_old (fresh_id [] x) gl in
 		let newl' = List.map (replace_term c (mkVar id)) l' in
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
 		  (atomize_list newl')
-                with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in
+                with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e 
+                end in
   Tacticals.New.tclTHENLIST
     [
       (atomize_list lc);
@@ -3370,7 +3394,8 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
    args *)
 let induct_destruct isrec with_evars (lc,elim,names,cls) =
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
-  Tacmach.New.of_old (is_functional_induction elim) >>= fun ifi ->
+  Proofview.Goal.enter begin fun gl ->
+  let ifi = Tacmach.New.of_old (is_functional_induction elim) gl in
   if Int.equal (List.length lc) 1 && not ifi then
     (* standard induction *)
     onOpenInductionArg
@@ -3385,7 +3410,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
       str "Example: induction x1 x2 x3 using my_scheme.");
     if not (Option.is_empty cls) then
       error "'in' clause not supported here.";
-    Tacmach.New.pf_apply finish_evar_resolution >>= fun finish_evar_resolution ->
+    let finish_evar_resolution = Tacmach.New.pf_apply finish_evar_resolution gl in
     let lc = List.map
       (map_induction_arg finish_evar_resolution) lc in
     begin match lc with
@@ -3407,6 +3432,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
       new_induct_gen_l isrec with_evars elim names newlc
     end
   end
+  end
 
 let induction_destruct isrec with_evars = function
   | [],_,_ -> Proofview.tclUNIT ()
@@ -3494,13 +3520,15 @@ let case_type t gl =
  *)
 
 let andE id =
-  Tacmach.New.pf_get_hyp_typ id >>= fun t ->
-  Tacmach.New.of_old pf_hnf_constr >>= fun hnf_constr ->
+  Proofview.Goal.enter begin fun gl ->
+  let t = Tacmach.New.pf_get_hyp_typ id gl in
+  let hnf_constr = Tacmach.New.of_old pf_hnf_constr gl in
   if is_conjunction (hnf_constr t) then
     (Tacticals.New.tclTHEN (simplest_elim (mkVar id)) (Tacticals.New.tclDO 2 intro))
   else
     Proofview.tclZERO (Errors.UserError (
       "andE" , (str("Tactic andE expects "^(Id.to_string id)^" is a conjunction."))))
+  end
 
 let dAnd cls =
   Tacticals.New.onClause
@@ -3510,13 +3538,15 @@ let dAnd cls =
     cls
 
 let orE id =
-  Tacmach.New.pf_get_hyp_typ id >>= fun t ->
-  Tacmach.New.of_old pf_hnf_constr >>= fun hnf_constr ->
+  Proofview.Goal.enter begin fun gl ->
+  let t = Tacmach.New.pf_get_hyp_typ id gl in
+  let hnf_constr = Tacmach.New.of_old pf_hnf_constr gl in
   if is_disjunction (hnf_constr t) then
     (Tacticals.New.tclTHEN (simplest_elim (mkVar id)) intro)
   else
     Proofview.tclZERO (Errors.UserError (
       "orE" , (str("Tactic orE expects "^(Id.to_string id)^" is a disjunction."))))
+  end
 
 let dorE b cls =
   Tacticals.New.onClause
@@ -3526,8 +3556,9 @@ let dorE b cls =
     cls
 
 let impE id =
-  Tacmach.New.pf_get_hyp_typ id >>= fun t ->
-  Tacmach.New.of_old pf_hnf_constr >>= fun hnf_constr ->
+  Proofview.Goal.enter begin fun gl ->
+  let t = Tacmach.New.pf_get_hyp_typ id gl in
+  let hnf_constr = Tacmach.New.of_old pf_hnf_constr gl in
   if is_imp_term (hnf_constr t) then
     let (dom, _, rng) = destProd (hnf_constr t) in
     Tacticals.New.tclTHENLAST
@@ -3537,6 +3568,7 @@ let impE id =
     Proofview.tclZERO (Errors.UserError (
       "impE" , (str("Tactic impE expects "^(Id.to_string id)^
 	      " is a an implication."))))
+  end
 
 let dImp cls =
   Tacticals.New.onClause
@@ -3644,7 +3676,8 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 
 let symmetry_in id =
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+  Proofview.Goal.enter begin fun gl ->
+  let type_of = Tacmach.New.pf_apply Typing.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
@@ -3664,6 +3697,7 @@ let symmetry_in id =
       | e -> Proofview.tclZERO e
     end
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let intros_symmetry =
   Tacticals.New.onClause