More Proofview.Goal.enter.

Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.

This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.

This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.

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

13 files changed, 584 insertions, 448 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 35b0dc7ff8..728eaa3fe6 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1275,17 +1275,21 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
 let rec trivial_fail_db dbg mod_delta db_list local_db =
   let intro_tac =
     Tacticals.New.tclTHEN (dbg_intro dbg)
-      ( Proofview.tclEVARMAP >= fun sigma ->
-        Proofview.Goal.env >>= fun env ->
-        Tacmach.New.pf_last_hyp >>= fun hyp ->
-	let hintl = make_resolve_hyp env sigma hyp
-	in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl 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 hintl = make_resolve_hyp env sigma hyp
+	  in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
+      end)
   in
-  Proofview.Goal.concl >>= fun concl ->
-  Tacticals.New.tclFIRST
-    ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
-     (List.map Tacticals.New.tclCOMPLETE
-       (trivial_resolve dbg mod_delta db_list local_db concl)))
+  Proofview.Goal.enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    Tacticals.New.tclFIRST
+      ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
+          (List.map Tacticals.New.tclCOMPLETE
+             (trivial_resolve dbg mod_delta db_list local_db concl)))
+  end
 
 and my_find_search_nodelta db_list local_db hdc concl =
   List.map (fun hint -> (None,hint))
@@ -1433,12 +1437,14 @@ let search d n mod_delta db_list local_db =
       if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
         Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
-	     ( Proofview.Goal.concl >>= fun concl ->
+	     ( Proofview.Goal.enter begin fun gl ->
+               let concl = Proofview.Goal.concl gl in
 	       let d' = incr_dbg d in
 	       Tacticals.New.tclFIRST
 	         (List.map
 		    (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
-		    (possible_resolve d mod_delta db_list local_db concl))))
+		    (possible_resolve d mod_delta db_list local_db concl))
+             end))
     end []
   in
   search d n local_db
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1aaf4af00b..c33e5fb7c3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -83,13 +83,17 @@ let rec eq_constr_mod_evars x y =
   | _, _ -> compare_constr eq_constr_mod_evars x y
 
 let progress_evars t =
-  Proofview.Goal.concl >>= fun concl ->
-  let check =
-      Proofview.Goal.concl >>= fun newconcl ->
-      if eq_constr_mod_evars concl newconcl
-      then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
-      else Proofview.tclUNIT ()
-  in t <*> check
+  Proofview.Goal.enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    let check =
+      Proofview.Goal.enter begin fun gl' ->
+        let newconcl = Proofview.Goal.concl gl' in
+        if eq_constr_mod_evars concl newconcl
+        then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
+        else Proofview.tclUNIT ()
+      end
+    in t <*> check
+  end
 
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 74780a8d23..c500a5969d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -44,19 +44,22 @@ let filter_hyp f tac =
     | [] -> Proofview.tclZERO Not_found
     | (id,_,t)::rest when f t -> tac id
     | _::rest -> seek rest in
-  Proofview.Goal.hyps >>= fun hyps ->
-  seek (Environ.named_context_of_val hyps)
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps gl in
+    seek (Environ.named_context_of_val hyps)
+  end
 
 let contradiction_context =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  let rec seek_neg l = match l with
-    | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
-    | (id,_,typ)::rest ->
-	let typ = whd_betadeltaiota env sigma typ in
-	if is_empty_type typ then
-	  simplest_elim (mkVar id)
-	else match kind_of_term typ with
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    let rec seek_neg l = match l with
+      | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
+      | (id,_,typ)::rest ->
+	  let typ = whd_betadeltaiota env sigma typ in
+	  if is_empty_type typ then
+	    simplest_elim (mkVar id)
+	  else match kind_of_term typ with
 	  | Prod (na,t,u) when is_empty_type u ->
 	      (Proofview.tclORELSE
                  begin
@@ -69,10 +72,11 @@ let contradiction_context =
                    | e -> Proofview.tclZERO e
                  end)
 	  | _ -> seek_neg rest
-  in
-  Proofview.Goal.hyps >>= fun hyps ->
-  let hyps = Environ.named_context_of_val hyps in
-  seek_neg hyps
+    in
+    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Environ.named_context_of_val hyps in
+    seek_neg hyps
+  end
 
 let is_negation_of env sigma typ t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
@@ -80,28 +84,30 @@ let is_negation_of env sigma typ t =
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-  try (* type_of can raise exceptions. *)
-  let typ = type_of c in
-  let _, ccl = splay_prod env sigma typ in
-  if is_empty_type ccl then
-    Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption))
-  else
-    Proofview.tclORELSE
-      begin
-        if lbind = NoBindings then
-	  filter_hyp (is_negation_of env sigma typ)
-	    (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
-        else
-	  Proofview.tclZERO Not_found
-      end
-      begin function
-        | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
-        | e -> Proofview.tclZERO e
-      end
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  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 ->
+    try (* type_of can raise exceptions. *)
+      let typ = type_of c in
+      let _, ccl = splay_prod env sigma typ in
+      if is_empty_type ccl then
+        Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption))
+      else
+        Proofview.tclORELSE
+          begin
+            if lbind = NoBindings then
+	      filter_hyp (is_negation_of env sigma typ)
+	        (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
+            else
+	      Proofview.tclZERO Not_found
+          end
+          begin function
+            | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+            | e -> Proofview.tclZERO e
+          end
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let contradiction = function
   | None -> Tacticals.New.tclTHEN intros contradiction_context
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 0a6e7a0724..a0e8fcb884 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -130,16 +130,18 @@ let solveArg eqonleft op a1 a2 tac =
 let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.concl >>= fun concl ->
-      match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
-      let (mib,mip) = Global.lookup_inductive rectype in
-      let nparams   = mib.mind_nparams in
-      let getargs l = List.skipn nparams (snd (decompose_app l)) in
-      let rargs   = getargs rhs
-      and largs   = getargs lhs in
-      List.fold_right2
-        (solveArg eqonleft op) largs rargs
-        (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+      Proofview.Goal.enter begin fun gl ->
+        let concl = Proofview.Goal.concl gl in
+        match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
+          let (mib,mip) = Global.lookup_inductive rectype in
+          let nparams   = mib.mind_nparams in
+          let getargs l = List.skipn nparams (snd (decompose_app l)) in
+          let rargs   = getargs rhs
+          and largs   = getargs lhs in
+          List.fold_right2
+            (solveArg eqonleft op) largs rargs
+            (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+      end
     end
     begin function
       | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
@@ -155,16 +157,18 @@ let hd_app c = match kind_of_term c with
 let decideGralEquality =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.concl >>= fun concl ->
-      match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
-      Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
-      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."))
-      end >= fun rectype ->
-      (Tacticals.New.tclTHEN
-         (mkBranches c1 c2)
-         (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+      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 ->
+        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."))
+        end >= fun rectype ->
+          (Tacticals.New.tclTHEN
+             (mkBranches c1 c2)
+             (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+      end
     end
     begin function
       | PatternMatchingFailure ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ff35b4eeb2..782ca67d52 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -324,7 +324,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   | _ -> assert false
 
 let type_of_clause = function
-  | None -> Proofview.Goal.concl
+  | None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl))
   | Some id -> Tacmach.New.pf_get_hyp_typ id
 
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
@@ -359,8 +359,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
   if occs != AllOccurrences then (
     rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
-    Proofview.tclEVARMAP >= fun sigma ->
-    Proofview.Goal.env >>= fun env ->
+    Proofview.Goal.enter begin fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
+      let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type t with
@@ -391,6 +392,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	            | None -> Proofview.tclZERO e
             (* error "The provided term does not end with an equality or a declared rewrite relation." *)  
             end
+    end
 
 let general_rewrite_ebindings =
   general_rewrite_ebindings_clause None
@@ -465,13 +467,16 @@ type delayed_open_constr_with_bindings =
 
 let general_multi_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
-    Proofview.tclEVARMAP >= fun sigma ->
-    Proofview.Goal.env >>= fun env ->
-    try (* f (an interpretation function) can raise exceptions *)
-      let sigma,c = f env sigma in
-      Tacticals.New.tclWITHHOLES with_evars
-        (general_multi_rewrite l2r with_evars ?tac c) sigma cl 
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in
+    Proofview.Goal.enter begin fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
+      let env = Proofview.Goal.env gl in
+      try (* f (an interpretation function) can raise exceptions *)
+        let sigma,c = f env sigma in
+        Tacticals.New.tclWITHHOLES with_evars
+          (general_multi_rewrite l2r with_evars ?tac c) sigma cl 
+      with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    end
+  in
   let rec doN l2r c = function
     | Precisely n when n <= 0 -> Proofview.tclUNIT ()
     | Precisely 1 -> do1 l2r c
@@ -848,15 +853,17 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.env >>= fun env ->
-  Proofview.Goal.concl >>= fun concl ->
-  match find_positions env sigma t1 t2 with
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    match find_positions env sigma t1 t2 with
     | 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
 	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 ->
@@ -877,16 +884,18 @@ let onEquality with_evars tac (c,lbindc) =
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 
 let onNegatedEquality with_evars tac =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.concl >>= fun ccl ->
-  Proofview.Goal.env >>= fun env ->
-  match kind_of_term (hnf_constr env sigma ccl) with
-  | Prod (_,t,u) when is_empty_type u ->
-      Tacticals.New.tclTHEN introf
-        (Tacticals.New.onLastHypId (fun id ->
-          onEquality with_evars tac (mkVar id,NoBindings)))
-  | _ ->
-      Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let ccl = Proofview.Goal.concl gl in
+    let env = Proofview.Goal.env gl in
+    match kind_of_term (hnf_constr env sigma ccl) with
+    | Prod (_,t,u) when is_empty_type u ->
+        Tacticals.New.tclTHEN introf
+          (Tacticals.New.onLastHypId (fun id ->
+            onEquality with_evars tac (mkVar id,NoBindings)))
+    | _ ->
+        Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+  end
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
@@ -1268,9 +1277,10 @@ let injConcl = injClause None false None
 let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
+  Proofview.Goal.enter begin fun gl ->
+    Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
     let sigma =  clause.evd in
-    Proofview.Goal.env >>= fun env ->
+    let env = Proofview.Goal.env gl in
       match find_positions env sigma t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn sort
@@ -1279,6 +1289,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
     | Inr posns ->
 	inject_at_positions env sigma true u clause posns
           (ntac (clenv_value clause))
+  end
 
 let dEqThen with_evars ntac = function
   | None -> onNegatedEquality with_evars (decompEqThen ntac)
@@ -1514,9 +1525,10 @@ let is_eq_x gl x (id,_,c) =
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
-  Proofview.Goal.env >>= fun env ->
-  Proofview.Goal.hyps >>= fun hyps ->
-  Proofview.Goal.concl >>= fun concl ->
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let hyps = Proofview.Goal.hyps gl in
+  let concl = Proofview.Goal.concl gl in
   let hyps = Environ.named_context_of_val hyps in
   (* The set of hypotheses using x *)
   let depdecls =
@@ -1551,29 +1563,32 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       else
        [Proofview.tclUNIT ()]) @
      [Proofview.V82.tactic (tclTRY (clear [x;hyp]))])
+  end
 
 (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
    it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one_var dep_proof_ok x =
-  Proofview.Goal.hyps >>= fun hyps ->
-  let hyps = Environ.named_context_of_val hyps in
-  Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) ->
-  (* 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: *)
-  let varx = mkVar x in
-  (* Find a non-recursive definition for x *)
-  let found gl =
-    try
-      let test hyp _ = is_eq_x gl varx hyp in
-      Context.fold_named_context test ~init:() hyps;
-      errorlabstrm "Subst"
-        (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) ->
-  subst_one dep_proof_ok x (hyp,rhs,dir)
+  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,_) ->
+    (* 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: *)
+      let varx = mkVar x in
+      (* Find a non-recursive definition for x *)
+      let found gl =
+        try
+          let test hyp _ = is_eq_x gl varx hyp in
+          Context.fold_named_context test ~init:() hyps;
+          errorlabstrm "Subst"
+            (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) ->
+      subst_one dep_proof_ok x (hyp,rhs,dir)
+  end
 
 let subst_gen dep_proof_ok ids =
   Tacticals.New.tclTHEN (Proofview.V82.tactic tclNORMEVAR) (Tacticals.New.tclMAP (subst_one_var dep_proof_ok) ids)
@@ -1651,9 +1666,11 @@ let rewrite_multi_assumption_cond cond_eq_term cl =
 	  with | Failure _ | UserError _ -> arec rest
 	end
   in
-  Proofview.Goal.hyps >>= fun hyps ->
-  let hyps = Environ.named_context_of_val hyps in
-  arec hyps
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Environ.named_context_of_val hyps in
+    arec hyps
+  end
 
 let replace_multi_term dir_opt c  =
   let cond_eq_fun =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 0555564bd1..20f72b3d56 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -53,8 +53,10 @@ let instantiate n (ist,rawc) ido gl =
 open Proofview.Notations
 let let_evar name typ =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  let sigma',evar = Evarutil.new_evar sigma env ~src typ in
-  Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
-    (Tactics.letin_tac None name evar None Locusops.nowhere)
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    let sigma',evar = Evarutil.new_evar sigma env ~src typ in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
+      (Tactics.letin_tac None name evar None Locusops.nowhere)
+  end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a4765f22b5..fcb1311617 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -664,9 +664,9 @@ let  mkCaseEq a  : unit Proofview.tactic =
       Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) >>= fun type_of_a ->
        Tacticals.New.tclTHENLIST
          [Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
-          begin
-            Proofview.Goal.concl >>= fun concl ->
-            Proofview.Goal.env >>= fun env ->
+          Proofview.Goal.enter begin fun gl ->
+            let concl = Proofview.Goal.concl gl in
+            let env = Proofview.Goal.env gl in
             Proofview.V82.tactic begin
 	      change_in_concl None
 	        (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)
@@ -683,8 +683,8 @@ let case_eq_intros_rewrite x =
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
-    begin
-      Proofview.Goal.concl >>= fun concl ->
+    Proofview.Goal.enter begin fun gl ->
+      let concl = Proofview.Goal.concl gl in
       Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
       let n' = nb_prod concl in
       Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>= fun h ->
@@ -719,7 +719,7 @@ let destauto_in id =
   destauto ctype
 
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.concl >>= fun concl -> destauto concl ]
+| [ "destauto" ] -> [ Proofview.Goal.enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e4d4fc80e6..b3c8b2837e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -443,44 +443,46 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
 
 
 let raw_inversion inv_kind id status names =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  Proofview.Goal.concl >>= fun concl ->
-  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 ->
-  begin
-    try
-      Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
-    with UserError _ ->
-      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 ccl = clenv_type indclause in
-  check_no_metas indclause ccl;
-  let IndType (indf,realargs) = find_rectype env sigma ccl in
-  let (elim_predicate,neqns) =
-    make_inv_predicate env sigma indf realargs id status concl in
-  let (cut_concl,case_tac) =
-    if status != NoDep & (dependent c concl) then
-      Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
-      Tacticals.New.case_then_using
-    else
-      Reduction.beta_appvect elim_predicate (Array.of_list realargs),
-      Tacticals.New.case_nodep_then_using
-  in
-  (Tacticals.New.tclTHENS
-     (assert_tac Anonymous cut_concl)
-     [case_tac names
-       (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
-       (Some elim_predicate) ([],[]) ind indclause;
-      Tacticals.New.onLastHypId
-        (fun id ->
-           (Tacticals.New.tclTHEN
-              (Proofview.V82.tactic (apply_term (mkVar id)
-                 (List.init neqns (fun _ -> Evarutil.mk_new_meta()))))
-              reflexivity))])
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    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 ->
+    begin
+      try
+        Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
+      with UserError _ ->
+        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 ccl = clenv_type indclause in
+      check_no_metas indclause ccl;
+      let IndType (indf,realargs) = find_rectype env sigma ccl in
+      let (elim_predicate,neqns) =
+        make_inv_predicate env sigma indf realargs id status concl in
+      let (cut_concl,case_tac) =
+        if status != NoDep & (dependent c concl) then
+          Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
+          Tacticals.New.case_then_using
+        else
+          Reduction.beta_appvect elim_predicate (Array.of_list realargs),
+          Tacticals.New.case_nodep_then_using
+      in
+      (Tacticals.New.tclTHENS
+         (assert_tac Anonymous cut_concl)
+         [case_tac names
+             (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
+             (Some elim_predicate) ([],[]) ind indclause;
+          Tacticals.New.onLastHypId
+            (fun id ->
+              (Tacticals.New.tclTHEN
+                 (Proofview.V82.tactic (apply_term (mkVar id)
+                                          (List.init neqns (fun _ -> Evarutil.mk_new_meta()))))
+                 reflexivity))])
+  end
 
 (* Error messages of the inversion tactics *)
 let wrap_inv_error id = function
@@ -523,25 +525,29 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
  * back to their places in the hyp-list. *)
 
 let invIn k names ids id =
-  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
-  Proofview.Goal.concl >>= fun concl ->
-  let nb_prod_init = nb_prod concl in
-  let intros_replace_ids =
-    Proofview.Goal.concl >>= fun concl ->
-    let nb_of_new_hyp =
-      nb_prod concl - (List.length hyps + nb_prod_init)
+  Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+    let concl = Proofview.Goal.concl gl in
+    let nb_prod_init = nb_prod concl in
+    let intros_replace_ids =
+      Proofview.Goal.enter begin fun gl ->
+        let concl = Proofview.Goal.concl gl in
+        let nb_of_new_hyp =
+          nb_prod concl - (List.length hyps + nb_prod_init)
+        in
+        if nb_of_new_hyp < 1 then
+          intros_replacing ids
+        else
+          Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)
+      end
     in
-    if nb_of_new_hyp < 1 then
-      intros_replacing ids
-    else
-      Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)
-  in
-  Proofview.tclORELSE
-    (Tacticals.New.tclTHENLIST
-      [Proofview.V82.tactic (bring_hyps hyps);
-       inversion (false,k) NoDep names id;
-       intros_replace_ids])
-    (wrap_inv_error id)
+    Proofview.tclORELSE
+      (Tacticals.New.tclTHENLIST
+         [Proofview.V82.tactic (bring_hyps hyps);
+          inversion (false,k) NoDep names id;
+          intros_replace_ids])
+      (wrap_inv_error id)
+  end
 
 let invIn_gen k names idl = try_intros_until (invIn k names idl)
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 04819830e5..e726e76921 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -284,17 +284,19 @@ let lemInv id c gls =
 let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
 
 let lemInvIn id c ids =
-  Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
-  let intros_replace_ids =
-    Proofview.Goal.concl >>= fun concl ->
-    let nb_of_new_hyp  = nb_prod concl - List.length ids in
-    if nb_of_new_hyp < 1  then
-      intros_replacing ids
-    else
-      (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids))
-  in
-  ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c)))
-    (intros_replace_ids)))
+  Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+    let intros_replace_ids =
+      let concl = Proofview.Goal.concl gl in
+      let nb_of_new_hyp  = nb_prod concl - List.length ids in
+      if nb_of_new_hyp < 1  then
+        intros_replacing ids
+      else
+        (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids))
+    in
+    ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c)))
+        (intros_replace_ids)))
+  end
 
 let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 66b2c64b0f..14a9eb0ed6 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1764,37 +1764,39 @@ let not_declared env ty rel =
 		str ty ++ str" relation. Maybe you need to require the Setoid library")
 
 let setoid_proof ty fn fallback =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
-  Proofview.Goal.concl >>= fun concl ->
-  Proofview.tclORELSE
-    begin
-      try
-        let rel, args = decompose_app_rel env sigma concl in
-        let evm = sigma in
-        let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
-        fn env evm car rel
-      with e -> Proofview.tclZERO e
-    end
-    begin function
-      | e ->
-        Proofview.tclORELSE
-          fallback
-          begin function
-            | Hipattern.NoEquationFound ->
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    Proofview.tclORELSE
+      begin
+        try
+          let rel, args = decompose_app_rel env sigma concl in
+          let evm = sigma in
+          let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
+          fn env evm car rel
+        with e -> Proofview.tclZERO e
+      end
+      begin function
+        | e ->
+            Proofview.tclORELSE
+              fallback
+              begin function
+                | Hipattern.NoEquationFound ->
                 (* spiwack: [Errors.push] here is unlikely to do what
                    it's intended to, or anything meaningful for that
                    matter. *)
-                let e = Errors.push e in
-	        begin match e with
-	        | Not_found ->
-	            let rel, args = decompose_app_rel env sigma concl in
-		    not_declared env ty rel
-	        | _ -> Proofview.tclZERO e
-                end
-            | e' -> Proofview.tclZERO e'
-          end
-    end
+                    let e = Errors.push e in
+	            begin match e with
+	            | Not_found ->
+	                let rel, args = decompose_app_rel env sigma concl in
+		        not_declared env ty rel
+	            | _ -> Proofview.tclZERO e
+                    end
+                | e' -> Proofview.tclZERO e'
+              end
+      end
+  end
 
 let setoid_reflexivity =
   setoid_proof "reflexive"
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index abc1daa5b8..83958eca28 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1265,11 +1265,13 @@ and interp_app loc ist fv largs =
         end >>== fun v ->
         (* No errors happened, we propagate the trace *)
         let v = append_trace trace v in
-        Proofview.Goal.env >>== fun env ->
-        Proofview.tclLIFT begin
-          debugging_step ist
-	    (fun () ->
-	      str"evaluation returns"++fnl()++pr_value (Some env) v)
+        Proofview.Goal.enter begin fun gl ->
+          let env = Proofview.Goal.env gl in
+          Proofview.tclLIFT begin
+            debugging_step ist
+	      (fun () ->
+	        str"evaluation returns"++fnl()++pr_value (Some env) v)
+          end 
         end <*>
         if List.is_empty lval then (Proofview.Goal.return v) else interp_app loc ist v lval
       else
@@ -1343,9 +1345,13 @@ and interp_letin ist llc u =
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
-  Proofview.Goal.enterl begin fun env sigma hyps concl ->
+  Proofview.Goal.enterl begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
+  let hyps = Proofview.Goal.hyps gl in
   let hyps = Environ.named_context_of_val hyps in
   let hyps = if lr then List.rev hyps else hyps in
+  let concl = Proofview.Goal.concl gl in
   let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
     let rec match_next_pattern next = match IStream.peek next with
     | None -> Proofview.tclZERO PatternMatchingFailure
@@ -1428,7 +1434,8 @@ and interp_match_goal ist lz lr lmr =
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
-  Proofview.Goal.env >>== fun env ->
+  Proofview.Goal.enterl begin fun gl ->
+    let env = Proofview.Goal.env gl in
   let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
     | hyp_pat::tl ->
 	let (hypname, _, pat as hyp_pat) =
@@ -1467,6 +1474,7 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
         eval_with_fail {ist with lfun=lfun} lz mt
   in
   apply_hyps_context_rec lctxt lgmatch hyps mhyps
+  end
 
 and interp_external loc ist gl com req la = assert false
 (* arnaud: todo
@@ -1582,11 +1590,13 @@ and interp_match ist lz constr lmr =
         in
         Proofview.tclORELSE begin match matches with
         | None -> let e = PatternMatchingFailure in
-                  (Proofview.Goal.env >>= fun env ->
-                  Proofview.tclLIFT begin
-                    debugging_exception_step ist false e (fun () ->
-                      str "matching with pattern" ++ fnl () ++
-                        pr_constr_pattern_env env c)
+                  (Proofview.Goal.enter begin fun gl ->
+                   let env = Proofview.Goal.env gl in
+                   Proofview.tclLIFT begin
+                     debugging_exception_step ist false e (fun () ->
+                       str "matching with pattern" ++ fnl () ++
+                         pr_constr_pattern_env env c)
+                   end
                   end) <*> Proofview.tclZERO e
         | Some lmatch ->
            Proofview.tclORELSE
@@ -1596,12 +1606,14 @@ and interp_match ist lz constr lmr =
              end
              begin function
                | e ->
-                   (Proofview.Goal.env >>= fun env ->
-                    Proofview.tclLIFT begin
-                      debugging_exception_step ist false e (fun () ->
-                        str "rule body for pattern" ++
-                          pr_constr_pattern_env env c)
-                    end) <*>
+                   (Proofview.Goal.enter begin fun gl ->
+                     let env = Proofview.Goal.env gl in
+                     Proofview.tclLIFT begin
+                       debugging_exception_step ist false e (fun () ->
+                         str "rule body for pattern" ++
+                           pr_constr_pattern_env env c)
+                     end
+                   end) <*>
                    Proofview.tclZERO e
              end
         end
@@ -1635,7 +1647,9 @@ and interp_match ist lz constr lmr =
           Proofview.tclZERO e
     end
   end >>== fun csr ->
-  Proofview.Goal.enterl begin fun env sigma _ _ ->
+  Proofview.Goal.enterl begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
     let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
     Proofview.tclORELSE
       (apply_match ist csr ilr)
@@ -1655,17 +1669,20 @@ and interp_ltac_constr ist e =
       (val_interp ist e)
       begin function
         | Not_found ->
-            (Proofview.Goal.env >>= fun env ->
-            Proofview.tclLIFT begin
-              debugging_step ist (fun () ->
-                str "evaluation failed for" ++ fnl() ++
-                  Pptactic.pr_glob_tactic env e)
+            (Proofview.Goal.enter begin fun gl ->
+              let env = Proofview.Goal.env gl in
+              Proofview.tclLIFT begin
+                debugging_step ist (fun () ->
+                  str "evaluation failed for" ++ fnl() ++
+                    Pptactic.pr_glob_tactic env e)
+              end
             end) <*>
             Proofview.tclZERO Not_found
         | e -> Proofview.tclZERO e
       end
   end >>== fun result ->
-  Proofview.Goal.env >>== fun env ->
+  Proofview.Goal.enterl begin fun gl ->
+    let env = Proofview.Goal.env gl in
   let result = Value.normalize result in
   try
     let cresult = coerce_to_closed_constr env result in
@@ -1677,11 +1694,13 @@ and interp_ltac_constr ist e =
     end <*>
     (Proofview.Goal.return cresult)
   with CannotCoerceTo _ ->
-    Proofview.Goal.env >>== fun env ->
+    let env = Proofview.Goal.env gl in
     Proofview.tclZERO (UserError ( "",
       errorlabstrm ""
       (str "Must evaluate to a closed term" ++ fnl() ++
       str "offending expression: " ++ fnl() ++ pr_inspect env e result)))
+  end
+
 
 (* Interprets tactic expressions : returns a "tactic" *)
 and interp_tactic ist tac =
@@ -1701,9 +1720,11 @@ and interp_atomic ist tac =
       with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacIntroMove (ido,hto) ->
-      Proofview.Goal.env >>= fun env ->
-      Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
-      h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
+      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 ->
+        h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
+      end
   | TacAssumption -> Proofview.V82.tactic h_assumption
   | TacExact c ->
       Proofview.V82.tactic begin fun gl -> 
@@ -1730,7 +1751,9 @@ and interp_atomic ist tac =
           gl
       end
   | TacApply (a,ev,cb,cl) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         try (* interp_open_constr_with_bindings_loc can raise exceptions *)
           let sigma, l =
             List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
@@ -1745,7 +1768,9 @@ and interp_atomic ist tac =
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacElim (ev,cb,cbo) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in 
         try (* interpretation functions may raise exceptions *)
           let sigma, cb = interp_constr_with_bindings ist env sigma cb in
           let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
@@ -1761,7 +1786,9 @@ and interp_atomic ist tac =
           gl
       end
   | TacCase (ev,cb) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
       end
@@ -1774,11 +1801,13 @@ and interp_atomic ist tac =
           gl
       end
   | TacFix (idopt,n) ->
-      Proofview.Goal.env >>= fun env ->
-      Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
+      end
   | TacMutualFix (id,n,l) ->
-      Proofview.Goal.env >>= fun env ->
-      Proofview.V82.tactic begin fun gl -> 
+      Proofview.V82.tactic begin fun gl ->
+        let env = pf_env gl in
         let f sigma (id,n,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
 	  sigma , (interp_fresh_ident ist env id,n,c_interp) in
@@ -1794,11 +1823,13 @@ and interp_atomic ist tac =
           gl
       end
   | TacCofix idopt ->
-      Proofview.Goal.env >>= fun env ->
-      Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
+      end
   | TacMutualCofix (id,l) ->
-      Proofview.Goal.env >>= fun env ->
-      Proofview.V82.tactic begin fun gl -> 
+      Proofview.V82.tactic begin fun gl ->
+        let env = pf_env gl in
         let f sigma (id,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
 	  sigma , (interp_fresh_ident ist env id,c_interp) in
@@ -1822,7 +1853,9 @@ and interp_atomic ist tac =
           gl
       end
   | TacAssert (t,ipat,c) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        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 ->
@@ -1833,11 +1866,11 @@ and interp_atomic ist tac =
         with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
       end
   | TacGeneralize cl ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
-        Proofview.V82.tactic begin fun gl -> 
-          let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
-          tclWITHHOLES false (h_generalize_gen) sigma cl gl
-        end
+      Proofview.V82.tactic begin fun gl ->
+        let sigma = project gl in
+        let env = pf_env gl in
+        let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
+        tclWITHHOLES false (h_generalize_gen) sigma cl gl
       end
   | TacGeneralizeDep c ->
       Proofview.V82.tactic begin fun gl -> 
@@ -1848,7 +1881,9 @@ and interp_atomic ist tac =
           gl
       end
   | TacLetTac (na,c,clp,b,eqpat) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      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 ->
         if Locusops.is_nowhere clp then
@@ -1868,13 +1903,17 @@ and interp_atomic ist tac =
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         Auto.h_trivial ~debug
 	  (interp_auto_lemmas ist env sigma lems)
 	  (Option.map (List.map (interp_hint_base ist)) l)
       end
   | TacAuto (debug,n,lems,l) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
 	  (interp_auto_lemmas ist env sigma lems)
 	  (Option.map (List.map (interp_hint_base ist)) l)
@@ -1884,25 +1923,27 @@ and interp_atomic ist tac =
   | TacSimpleInductionDestruct (isrec,h) ->
       h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
-      Proofview.Goal.env >>= fun env ->
-      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
-        end l
-      in
-      Proofview.tclEVARMAP >= fun sigma ->
-      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 cls = Option.map interp_clause cls in
-      Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
+      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
+          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 cls = Option.map interp_clause cls in
+        Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
+      end
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
@@ -1924,7 +1965,9 @@ and interp_atomic ist tac =
 	(Proofview.V82.tclEVARS sigma)
 	(Elim.h_decompose l c_interp)
   | TacSpecialize (n,cb) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
           let sigma, cb = interp_constr_with_bindings ist env sigma cb in
           tclWITHHOLES false (h_specialize n) sigma cb gl
@@ -1953,8 +1996,8 @@ and interp_atomic ist tac =
         h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) gl
       end
   | TacRename l ->
-      Proofview.Goal.env >>= fun env ->
-      Proofview.V82.tactic begin fun gl -> 
+      Proofview.V82.tactic begin fun gl ->
+        let env = pf_env gl in
         h_rename (List.map (fun (id1,id2) ->
 	  interp_hyp ist gl id1,
 	  interp_fresh_ident ist env (snd id2)) l)
@@ -1967,24 +2010,32 @@ and interp_atomic ist tac =
 
   (* Constructors *)
   | TacLeft (ev,bl) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
         Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
       end
   | TacRight (ev,bl) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
         Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
       end
   | TacSplit (ev,_,bll) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
         Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
       end
   | TacAnyConstructor (ev,t) ->
       Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
   | TacConstructor (ev,n,bl) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         let sigma, bl = interp_bindings ist env sigma bl in
         Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
       end
@@ -2019,7 +2070,9 @@ and interp_atomic ist tac =
           gl
       end
   | TacChange (Some op,c,cl) ->
-      Proofview.Goal.enter begin fun env sigma _ _ ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
           let sign,op = interp_typed_pattern ist env sigma op in
         (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
@@ -2104,7 +2157,8 @@ and interp_atomic ist tac =
       Proofview.V82.tclEVARS sigma <*>
       tac args ist
   | TacAlias (loc,s,l,(_,body)) ->
-      Proofview.Goal.env >>= fun env ->
+      Proofview.Goal.enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
       let rec f x = match genarg_tag x with
           | IntOrVarArgType ->
               (Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
@@ -2195,6 +2249,7 @@ and interp_atomic ist tac =
         lfun = lfun;
         extra = TacStore.set ist.extra f_trace trace; } in
       interp_tactic ist body
+      end
 
 (* Initial call for interpretation *)
 
@@ -2211,7 +2266,9 @@ let eval_tactic t =
 
 
 let interp_tac_gen lfun avoid_ids debug t =
-  Proofview.Goal.enter begin fun env sigma _ _ ->
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
   let ist = { lfun = lfun; extra = extra } in
@@ -2232,7 +2289,9 @@ let eval_ltac_constr t =
 
 (* Used to hide interpretation for pretty-print, now just launch tactics *)
 let hide_interp t ot =
-  Proofview.Goal.enter begin fun env sigma _ _ ->
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
     let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
                 gsigma = sigma; genv = env } in
     let te = intern_pure_tactic ist t in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 74c31fa382..5d3c8b97ab 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -522,27 +522,35 @@ module New = struct
         | e -> Proofview.tclZERO e
       end
 
-  let nthDecl m =
-    Proofview.Goal.hyps >>== fun hyps ->
+  let nthDecl m gl =
+    let hyps = Proofview.Goal.hyps gl in
     try
       let hyps = Environ.named_context_of_val hyps in
-      (Proofview.Goal.return (List.nth hyps (m-1)))
-    with Failure _ -> tclZERO (UserError ("" , Pp.str"No such assumption."))
+      List.nth hyps (m-1)
+    with Failure _ -> Errors.error "No such assumption."
 
-  let nthHypId m = nthDecl m >>== fun (id,_,_) ->
-    Proofview.Goal.return id
-  let nthHyp m = nthHypId m >>== fun id ->
-    Proofview.Goal.return (mkVar id)
+  let nthHypId m gl =
+    let (id,_,_) = nthDecl m gl in
+    id
+  let nthHyp m gl = 
+    mkVar (nthHypId m gl)
 
   let onNthHypId m tac =
-    nthHypId m >>= tac
+    Goal.enter begin fun gl ->
+      Proofview.tclUNIT (nthHypId m gl) >= tac
+    end
   let onNthHyp m tac =
-    nthHyp m >>= tac
+    Goal.enter begin fun gl ->
+      Proofview.tclUNIT (nthHyp m gl) >= tac
+    end
 
   let onLastHypId = onNthHypId 1
   let onLastHyp   = onNthHyp 1
 
-  let onNthDecl m tac = nthDecl m >>= tac
+  let onNthDecl m tac =
+    Proofview.Goal.enter begin fun gl ->
+      Proofview.tclUNIT (nthDecl m gl) >= tac
+    end
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fe605da8ef..5e62451f9a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -460,8 +460,9 @@ let build_intro_tac id dest tac = match dest with
   | dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
 
 let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
-  Proofview.Goal.concl >>= fun concl ->
-  match kind_of_term concl with
+  Proofview.Goal.enter begin fun gl ->
+    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 ->
 	build_intro_tac name move_flag tac
@@ -476,14 +477,15 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
             (* probably also a pity that intro does zeta *)
           else Proofview.tclUNIT ()
         end <*>
-	Proofview.tclORELSE
+	  Proofview.tclORELSE
 	  (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
-	    (intro_then_gen loc name_flag move_flag false dep_flag tac))
+	     (intro_then_gen loc name_flag move_flag false dep_flag tac))
           begin function
             | RefinerError IntroNeedsProduct ->
                 Proofview.tclZERO (Loc.add_loc (Errors.UserError("Intro",str "No product even after head-reduction.")) loc)
             | e -> Proofview.tclZERO e
           end
+  end
 
 let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> Proofview.tclUNIT ())
 let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false
@@ -1281,18 +1283,20 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if i > nconstr then error "Not enough constructors."
 
 let constructor_tac with_evars expctdnumopt i lbind =
-  Proofview.Goal.concl >>= fun cl ->
-  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
-  try (* reduce_to_quantified_ind can raise an exception *)
-  let (mind,redcl) = reduce_to_quantified_ind cl in
-  let nconstr =
-    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  check_number_of_constructors expctdnumopt i nconstr;
-  let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-  let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
-  (Tacticals.New.tclTHENLIST
-     [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  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 ->
+    try (* reduce_to_quantified_ind can raise an exception *)
+      let (mind,redcl) = reduce_to_quantified_ind cl in
+      let nconstr =
+        Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
+      check_number_of_constructors expctdnumopt i nconstr;
+      let cons = mkConstruct (ith_constructor_of_inductive mind i) in
+      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
+      (Tacticals.New.tclTHENLIST
+         [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let one_constructor i lbind = constructor_tac false None i lbind
 
@@ -1303,18 +1307,20 @@ let one_constructor i lbind = constructor_tac false None i lbind
 
 let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
-  Proofview.Goal.concl >>= fun cl ->
-  Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+  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 ->
   try (* reduce_to_quantified_ind can raise an exception *)
-  let mind = fst (reduce_to_quantified_ind cl) in
-  let nconstr =
-    Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if Int.equal nconstr 0 then error "The type has no constructors.";
-  Tacticals.New.tclFIRST
-    (List.map
-      (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t)
-      (List.interval 1 nconstr))
+    let mind = fst (reduce_to_quantified_ind cl) in
+    let nconstr =
+      Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
+    if Int.equal nconstr 0 then error "The type has no constructors.";
+    Tacticals.New.tclFIRST
+      (List.map
+         (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t)
+         (List.interval 1 nconstr))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
 
 let left_with_bindings  with_evars = constructor_tac with_evars (Some 2) 1
 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
@@ -1400,29 +1406,31 @@ let rewrite_hyp l2r id =
     Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
-  Proofview.Goal.env >>= fun env ->
-  Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
-  Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
-  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 *)
-  match match_with_equality_type t with
-  | Some (hdcncl,[_;lhs;rhs]) ->
-      if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
-	subst_on l2r (destVar lhs) rhs
-      else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
-	subst_on l2r (destVar rhs) lhs
-      else
-	Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
-  | Some (hdcncl,[c]) ->
-      let l2r = not l2r in (* equality of the form eq_true *)
-      if isVar c then
-	Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
-      else
-	Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
-  | _ ->
-      Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  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 ->
+    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 *)
+      match match_with_equality_type t with
+      | Some (hdcncl,[_;lhs;rhs]) ->
+          if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
+	    subst_on l2r (destVar lhs) rhs
+          else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
+	    subst_on l2r (destVar rhs) lhs
+          else
+	    Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+      | Some (hdcncl,[c]) ->
+          let l2r = not l2r in (* equality of the form eq_true *)
+          if isVar c then
+	    Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
+          else
+	    Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+      | _ ->
+          Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let rec explicit_intro_names = function
 | (_, IntroIdentifier id) :: l ->
@@ -1893,47 +1901,49 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
   (depdecls,lastlhyp,ccl,out test)
 
 let letin_tac_gen with_eq name (sigmac,c) test ty occs =
-  Proofview.Goal.env >>= fun env ->
-  Proofview.Goal.hyps >>= fun hyps ->
-  let hyps = Environ.named_context_of_val hyps in
-  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
-	  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
-    | 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 ->
-      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) ->
-  Tacticals.New.tclTHENLIST
-    [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
-      intro_gen dloc (IntroMustBe id) lastlhyp true false;
-      Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
-      eq_tac ]
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let hyps = Proofview.Goal.hyps gl in
+    let hyps = Environ.named_context_of_val hyps in
+    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
+	    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
+      | 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 ->
+            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) ->
+    Tacticals.New.tclTHENLIST
+      [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
+        intro_gen dloc (IntroMustBe id) lastlhyp true false;
+        Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
+        eq_tac ]
+  end
 
 let make_eq_test c = (make_eq_test c,fun _ -> c)
 
@@ -1942,11 +1952,13 @@ let letin_tac with_eq name c ty occs =
   letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true)
 
 let letin_pat_tac with_eq name c ty occs =
-  Proofview.tclEVARMAP >= fun sigma ->
-  Proofview.Goal.env >>= fun env ->
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
   letin_tac_gen with_eq name c
     (make_pattern_test env sigma c)
     ty (occs,true)
+  end
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c =
@@ -2162,6 +2174,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   let params = List.firstn nparams argl in
   (* le gl est important pour ne pas préévaluer *)
   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 ->
       (* If argl <> [], we expect typ0 not to be quantified, in order to
@@ -2170,7 +2183,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
       let indtyp = reduce_to_atomic_ref indref tmptyp0 in
       let argl = snd (decompose_app indtyp) in
       let c = List.nth argl (i-1) in
-      Proofview.Goal.env >>= fun env ->
+      let env = Proofview.Goal.env gl in
       match kind_of_term c with
 	| Var id when not (List.exists (occur_var env id) avoid) ->
 	    atomize_one (i-1) ((mkVar id)::avoid)
@@ -2189,6 +2202,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
 	      (atomize_one (i-1) ((mkVar x)::avoid))
     else
       Proofview.tclUNIT ()
+    end
   in
   atomize_one (List.length argl) params
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
@@ -3121,26 +3135,28 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
    hypotheses from the context *)
 
 let apply_induction_in_context hyp0 elim indvars names induct_tac =
-  Proofview.Goal.env >>= fun env ->
-  Proofview.Goal.concl >>= fun concl ->
-  let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
-  let deps = List.map (on_pi3 refresh_universes_strict) deps in
-  let tmpcl = it_mkNamedProd_or_LetIn concl deps in
-  let dephyps = List.map (fun (id,_,_) -> id) deps in
-  let deps_cstr =
-    List.fold_left
-      (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
-  Tacticals.New.tclTHENLIST
-    [
-      (* Generalize dependent hyps (but not args) *)
-      if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr);
-      (* clear dependent hyps *)
-      Proofview.V82.tactic (thin dephyps);
-      (* side-conditions in elim (resp case) schemes come last (resp first) *)
-      apply_induction_with_discharge
-	induct_tac elim (List.rev indhyps) lhyp0 (List.rev dephyps) names
-        (re_intro_dependent_hypotheses statuslists)
-    ]
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let concl = Proofview.Goal.concl gl in
+    let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+    let deps = List.map (on_pi3 refresh_universes_strict) deps in
+    let tmpcl = it_mkNamedProd_or_LetIn concl deps in
+    let dephyps = List.map (fun (id,_,_) -> id) deps in
+    let deps_cstr =
+      List.fold_left
+        (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
+    Tacticals.New.tclTHENLIST
+      [
+        (* Generalize dependent hyps (but not args) *)
+        if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr);
+        (* clear dependent hyps *)
+        Proofview.V82.tactic (thin dephyps);
+        (* side-conditions in elim (resp case) schemes come last (resp first) *)
+        apply_induction_with_discharge
+	  induct_tac elim (List.rev indhyps) lhyp0 (List.rev dephyps) names
+          (re_intro_dependent_hypotheses statuslists)
+      ]
+  end
 
 (* Induction with several induction arguments, main differences with
    induction_from_context is that there is no main induction argument,
@@ -3280,22 +3296,26 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	  (induction_with_atomization_of_ind_arg
 	    isrec with_evars elim names (id,lbind) inhyps)
     | _        ->
-        Proofview.tclEVARMAP >= fun defs ->
-        Proofview.Goal.env >>= fun env ->
-	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 ->
+        Proofview.Goal.enter begin fun gl ->
+          let defs = Proofview.Goal.sigma gl in
+          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 ->
 	(* We need the equality name now *)
-	let with_eq = Option.map (fun eq -> (false,eq)) eqname in
+	  let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
-        Proofview.Goal.env >>= fun env ->
-	Tacticals.New.tclTHEN
-          (* Warning: letin is buggy when c is not of inductive type *)
-	  (letin_tac_gen with_eq (Name id) (sigma,c)
-             (make_pattern_test env defs (sigma,c))
-             None (Option.default allHypsAndConcl cls,false))
-	  (induction_with_atomization_of_ind_arg
-	     isrec with_evars elim names (id,lbind) inhyps)
+          Proofview.Goal.enter begin fun gl ->
+            let env = Proofview.Goal.env gl in
+	    Tacticals.New.tclTHEN
+            (* Warning: letin is buggy when c is not of inductive type *)
+	      (letin_tac_gen with_eq (Name id) (sigma,c)
+                 (make_pattern_test env defs (sigma,c))
+                 None (Option.default allHypsAndConcl cls,false))
+	      (induction_with_atomization_of_ind_arg
+	         isrec with_evars elim names (id,lbind) inhyps)
+          end
+        end
 
 (* Induction on a list of arguments. First make induction arguments
    atomic (using letins), then do induction. The specificity here is