Merge PR#623: Remove the Sigma (monotonous state) API.

19 files changed, 713 insertions, 799 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e213965485..272cb1edaa 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -97,11 +97,11 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
   in clenv, c
 
 let unify_resolve poly flags ((c : raw_hint), clenv) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine false clenv
-  end }
+  end
 
 let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
 
@@ -110,12 +110,12 @@ let unify_resolve_gen poly = function
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let clenv', c = connect_hint_clenv poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
-  end }
+  end
 
 (* Util *)
 
@@ -141,7 +141,7 @@ let conclPattern concl pat tac =
 	with Constr_matching.PatternMatchingFailure ->
           Tacticals.New.tclZEROMSG (str "pattern-matching failed")
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
      let env = Proofview.Goal.env gl in
      let sigma = Tacmach.New.project gl in
        constr_bindings env sigma >>= fun constr_bindings ->
@@ -157,7 +157,7 @@ let conclPattern concl pat tac =
      match tac with
      | GenArg (Glbwit wit, tac) ->
       Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
-  end }
+  end
 
 (***********************************************************)
 (** A debugging / verbosity framework for trivial and auto *)
@@ -313,7 +313,7 @@ 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.Goal.enter { enter = begin fun gl ->
+      ( Proofview.Goal.enter begin fun gl ->
           let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
@@ -322,9 +322,9 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list
 	       (Hint_db.add_list env sigma hintl local_db)
-      end })
+      end)
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Tacmach.New.pf_concl gl in
     let sigma = Tacmach.New.project gl in
     let secvars = compute_secvars gl in
@@ -332,7 +332,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
       ((dbg_assumption dbg)::intro_tac::
           (List.map Tacticals.New.tclCOMPLETE
              (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl)))
-  end }
+  end
 
 and my_find_search_nodelta sigma db_list local_db secvars hdc concl =
   List.map (fun hint -> (None,hint))
@@ -375,7 +375,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
-    | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
+    | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
@@ -384,11 +384,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
     | Unfold_nth c ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
        if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
 	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
        else Tacticals.New.tclFAIL 0 (str"Unbound reference")
-       end }
+       end
     | Extern tacast -> 
       conclPattern concl p tacast
   in
@@ -417,7 +417,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
     "nocore" amongst the databases. *)
 
 let trivial ?(debug=Off) lems dbnames =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
@@ -425,10 +425,10 @@ let trivial ?(debug=Off) lems dbnames =
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
-  end }
+  end
 
 let full_trivial ?(debug=Off) lems =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
@@ -436,7 +436,7 @@ let full_trivial ?(debug=Off) lems =
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (trivial_fail_db d false db_list hints)
-  end }
+  end
 
 let gen_trivial ?(debug=Off) lems = function
   | None -> full_trivial ~debug lems
@@ -469,10 +469,10 @@ let extend_local_db decl db gl =
 
 let intro_register dbg kont db =
   Tacticals.New.tclTHEN (dbg_intro dbg)
-    (Proofview.Goal.enter { enter = begin fun gl ->
+    (Proofview.Goal.enter begin fun gl ->
       let extend_local_db decl db = extend_local_db decl db gl in
       Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
-    end })
+    end)
 
 (* n is the max depth of search *)
 (* local_db contains the local Hypotheses *)
@@ -485,7 +485,7 @@ let search d n mod_delta db_list local_db =
       if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
         Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
-	     ( Proofview.Goal.enter { enter = begin fun gl ->
+	     ( Proofview.Goal.enter begin fun gl ->
                let concl = Tacmach.New.pf_concl gl in
                let sigma = Tacmach.New.project gl in
                let secvars = compute_secvars gl in
@@ -494,7 +494,7 @@ let search d n mod_delta db_list local_db =
 	         (List.map
 		    (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
 		    (possible_resolve sigma d mod_delta db_list local_db secvars concl))
-             end }))
+             end))
     end []
   in
   search d n local_db
@@ -502,7 +502,7 @@ let search d n mod_delta db_list local_db =
 let default_search_depth = ref 5
 
 let delta_auto debug mod_delta n lems dbnames =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = make_db_list dbnames in
@@ -510,7 +510,7 @@ let delta_auto debug mod_delta n lems dbnames =
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (search d n mod_delta db_list hints)
-  end }
+  end
 
 let delta_auto = 
   if Flags.profile then
@@ -525,7 +525,7 @@ 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 { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let db_list = current_pure_db () in
@@ -533,7 +533,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems =
   let hints = make_local_hint_db env sigma false lems in
   tclTRY_dbg d
     (search d n mod_delta db_list hints)
-  end }
+  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/auto.mli b/tactics/auto.mli
index 9ed9f0ae26..a6fb82bab2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -16,14 +16,14 @@ open Decl_kinds
 open Hints
 open Tactypes
 
-val compute_secvars : ('a,'b) Proofview.Goal.t -> Id.Pred.t
+val compute_secvars : 'a Proofview.Goal.t -> Id.Pred.t
 
 val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-  ('a, 'r) Proofview.Goal.t -> clausenv * constr
+  'a Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index de544fe5f9..2d4f202769 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -15,7 +15,6 @@ open CErrors
 open Util
 open Mod_subst
 open Locus
-open Proofview.Notations
 
 (* Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
@@ -90,15 +89,14 @@ type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_gen
 let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = find_rewrites bas in
   let try_rewrite dir ctx c tc =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
     let c' = Vars.subst_univs_level_constr subst c in
-    let sigma = Sigma.to_evar_map sigma in
     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
-    let tac = general_rewrite_maybe_in dir c' tc in
-    Sigma.Unsafe.of_pair (tac, sigma)
-  end } in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (general_rewrite_maybe_in dir c' tc)
+  end in
   let lrul = List.map (fun h -> 
   let tac = match h.rew_tac with
   | None -> Proofview.tclUNIT ()
@@ -125,7 +123,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
       (Proofview.tclUNIT()) lbas))
 
 let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
  (* let's check at once if id exists (to raise the appropriate error) *)
   let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
   let general_rewrite_in id dir cstr tac =
@@ -137,7 +135,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 }
+ end
 
 let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]
 
@@ -162,10 +160,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
 	   | None ->
 		 (* try to rewrite in all hypothesis
 		    (except maybe the rewritten one) *)
-               Proofview.Goal.nf_enter { enter = begin fun gl ->
+               Proofview.Goal.nf_enter begin fun gl ->
                  let ids = Tacmach.New.pf_ids_of_hyps gl in
 		 try_do_hyps (fun id -> id)  ids
-               end })
+               end)
 
 let auto_multi_rewrite ?(conds=Naive) lems cl =
   Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 672f9cffb5..de49a521fd 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -211,7 +211,7 @@ let auto_unif_flags freeze st =
 
 let e_give_exact flags poly (c,clenv) =
   let open Tacmach.New in
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let (c, _, _) = c in
   let c, sigma =
@@ -223,34 +223,34 @@ let e_give_exact flags poly (c,clenv) =
     else c, sigma
   in
   let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
-  Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
-  end }
+  Proofview.Unsafe.tclEVARS sigma <*>
+  Clenvtac.unify ~flags t1 <*> exact_no_check c
+  end
 
 let clenv_unique_resolver_tac with_evars ~flags clenv' =
-  Proofview.Goal.enter { enter = begin fun gls ->
+  Proofview.Goal.enter begin fun gls ->
     let resolve =
       try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
       with e -> Proofview.tclZERO e
     in resolve >>= fun clenv' ->
        Clenvtac.clenv_refine with_evars ~with_classes:false clenv'
-  end }
+  end
 
-let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
+let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
-  clenv_unique_resolver_tac true ~flags clenv' end }
+  clenv_unique_resolver_tac true ~flags clenv' end
 
-let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
+let unify_resolve poly flags = begin fun gls (c,_,clenv) ->
   let clenv', _ = connect_hint_clenv poly c clenv gls in
   clenv_unique_resolver_tac false ~flags clenv'
-  end }
+  end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
 let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
   let open Clenv in
   let env = Proofview.Goal.env gls in
   let concl = Proofview.Goal.concl gls in
-  Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
-      let sigma = Sigma.to_evar_map sigma in
+  Refine.refine ~unsafe:true begin fun sigma ->
       let sigma, term, ty =
         if poly then
           let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
@@ -266,7 +266,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
       let sigma' =
         Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
                                 cl.cl_concl concl sigma'
-      in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
+      in (sigma', term) end
 
 let unify_resolve_refine poly flags gl clenv =
   Proofview.tclORELSE
@@ -297,32 +297,31 @@ let clenv_of_prods poly nprods (c, clenv) gl =
 
 let with_prods nprods poly (c, clenv) f =
   if get_typeclasses_limit_intros () then
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       try match clenv_of_prods poly nprods (c, clenv) gl with
           | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
-          | Some (diff, clenv') -> f.enter gl (c, diff, clenv')
+          | Some (diff, clenv') -> f gl (c, diff, clenv')
       with e when CErrors.noncritical e ->
-        Tacticals.New.tclZEROMSG (CErrors.print e) end }
+        Tacticals.New.tclZEROMSG (CErrors.print e) end
   else Proofview.Goal.enter
-         { enter = begin fun gl ->
-                   if Int.equal nprods 0 then f.enter gl (c, None, clenv)
-                   else Tacticals.New.tclZEROMSG (str"Not enough premisses") end }
+         begin fun gl ->
+         if Int.equal nprods 0 then f gl (c, None, clenv)
+         else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
 
 let matches_pattern concl pat =
   let matches env sigma =
     match pat with
     | None -> Proofview.tclUNIT ()
     | Some pat ->
-       let sigma = Sigma.to_evar_map sigma in
        if Constr_matching.is_matching env sigma pat concl then
          Proofview.tclUNIT ()
        else
          Tacticals.New.tclZEROMSG (str "pattern does not match")
   in
-   Proofview.Goal.enter { enter = fun gl ->
+   Proofview.Goal.enter begin fun gl ->
      let env = Proofview.Goal.env gl in
      let sigma = Proofview.Goal.sigma gl in
-       matches env sigma }
+       matches env sigma end
 
 (** Semantics of type class resolution lemma application:
 
@@ -363,7 +362,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
   let open Tacticals.New in
   let open Tacmach.New in
   let trivial_fail =
-    Proofview.Goal.enter { enter =
+    Proofview.Goal.enter
     begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -371,15 +370,15 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
     let hintl = make_resolve_hyp env sigma d in
     let hints = Hint_db.add_list env sigma hintl local_db in
       e_trivial_fail_db only_classes db_list hints secvars
-      end }
+      end
   in
   let trivial_resolve =
-    Proofview.Goal.enter { enter =
+    Proofview.Goal.enter
     begin fun gl ->
     let tacs = e_trivial_resolve db_list local_db secvars only_classes
                                  (project gl) (pf_concl gl) in
       tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs)
-    end}
+    end
   in
   let tacl =
     Eauto.registered_e_assumption ::
@@ -418,9 +417,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
            if get_typeclasses_filtered_unification () then
              let tac =
                with_prods nprods poly (term,cl)
-                          ({ enter = fun gl clenv ->
+                          (fun gl clenv ->
                              matches_pattern concl p <*>
-                               unify_resolve_refine poly flags gl clenv})
+                               unify_resolve_refine poly flags gl clenv)
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -433,9 +432,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
         | ERes_pf (term,cl) ->
            if get_typeclasses_filtered_unification () then
              let tac = (with_prods nprods poly (term,cl)
-                  ({ enter = fun gl clenv ->
+                  (fun gl clenv ->
                              matches_pattern concl p <*>
-                             unify_resolve_refine poly flags gl clenv})) in
+                             unify_resolve_refine poly flags gl clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
@@ -450,7 +449,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
              let tac =
                matches_pattern concl p <*>
                  Proofview.Goal.nf_enter
-                   { enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
+                   (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              e_give_exact flags poly (c,clenv)
@@ -1039,16 +1038,16 @@ module Search = struct
       sigma goals
 
   let fail_if_nonclass info =
-    Proofview.Goal.enter { enter = fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let gl = Proofview.Goal.assume gl in
-      let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+      let sigma = Proofview.Goal.sigma gl in
       if is_class_type sigma (Proofview.Goal.concl gl) then
         Proofview.tclUNIT ()
       else (if !typeclasses_debug > 1 then
               Feedback.msg_debug (pr_depth info.search_depth ++
                                     str": failure due to non-class subgoal " ++
                                     pr_ev sigma (Proofview.Goal.goal gl));
-            Proofview.tclZERO NoApplicableEx) }
+            Proofview.tclZERO NoApplicableEx) end
 
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
@@ -1060,18 +1059,17 @@ module Search = struct
     let env = Goal.env gl in
     let concl = Goal.concl gl in
     let sigma = Goal.sigma gl in
-    let s = Sigma.to_evar_map sigma in
-    let unique = not info.search_dep || is_unique env s concl in
-    let backtrack = needs_backtrack env s unique concl in
+    let unique = not info.search_dep || is_unique env sigma concl in
+    let backtrack = needs_backtrack env sigma unique concl in
     if !typeclasses_debug > 0 then
       Feedback.msg_debug
         (pr_depth info.search_depth ++ str": looking for " ++
-           Printer.pr_econstr_env (Goal.env gl) s concl ++
+           Printer.pr_econstr_env (Goal.env gl) sigma concl ++
            (if backtrack then str" with backtracking"
             else str" without backtracking"));
     let secvars = compute_secvars gl in
     let poss =
-      e_possible_resolve hints info.search_hints secvars info.search_only_classes s concl in
+      e_possible_resolve hints info.search_hints secvars info.search_only_classes sigma concl in
     (* If no goal depends on the solution of this one or the
        instances are irrelevant/assumed to be unique, then
        we don't need to backtrack, as long as no evar appears in the goal
@@ -1089,7 +1087,7 @@ module Search = struct
             pr_depth (idx :: info.search_depth) ++ str": " ++
               Lazy.force pp ++
               (if !foundone != true then
-                 str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
+                 str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl))
                else mt ())
           in
           let msg =
@@ -1104,15 +1102,14 @@ module Search = struct
           Feedback.msg_debug (header ++ str " failed with: " ++ msg)
         else ()
       in
-      let tac_of gls i j = Goal.enter { enter = fun gl' ->
+      let tac_of gls i j = Goal.enter begin fun gl' ->
         let sigma' = Goal.sigma gl' in
-        let s' = Sigma.to_evar_map sigma' in
         let _concl = Goal.concl gl' in
         if !typeclasses_debug > 0 then
           Feedback.msg_debug
             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
-               pr_ev s' (Proofview.Goal.goal (Proofview.Goal.assume gl')));
-        let eq c1 c2 = EConstr.eq_constr s' c1 c2 in
+               pr_ev sigma' (Proofview.Goal.goal (Proofview.Goal.assume gl')));
+        let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in
         let hints' =
           if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
           then
@@ -1120,7 +1117,7 @@ module Search = struct
             make_autogoal_hints info.search_only_classes ~st gl'
           else info.search_hints
         in
-        let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal (Proofview.Goal.assume gl')) gls in
+        let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal (Proofview.Goal.assume gl')) gls in
         let info' =
           { search_depth = succ j :: i :: info.search_depth;
             last_tac = pp;
@@ -1128,7 +1125,7 @@ module Search = struct
             search_only_classes = info.search_only_classes;
             search_hints = hints';
             search_cut = derivs }
-        in kont info' }
+        in kont info' end
       in
       let rec result (shelf, ()) i k =
         foundone := true;
@@ -1137,7 +1134,7 @@ module Search = struct
         (if !typeclasses_debug > 0 then
            Feedback.msg_debug
              (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp
-              ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
+              ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl))
               ++ str", " ++ int j ++ str" subgoal(s)" ++
                 (Option.cata (fun k -> str " in addition to the first " ++ int k)
                              (mt()) k)));
@@ -1207,7 +1204,7 @@ module Search = struct
          if !foundone == false && !typeclasses_debug > 0 then
            Feedback.msg_debug
              (pr_depth info.search_depth ++ str": no match for " ++
-                Printer.pr_econstr_env (Goal.env gl) s concl ++
+                Printer.pr_econstr_env (Goal.env gl) sigma concl ++
                 str ", " ++ int (List.length poss) ++
                 str" possibilities");
          match e with
@@ -1219,18 +1216,17 @@ module Search = struct
 
   let hints_tac hints info kont : unit Proofview.tactic =
     Proofview.Goal.enter
-      { enter = fun gl -> hints_tac_gl hints info kont gl }
+      (fun gl -> hints_tac_gl hints info kont gl)
 
   let intro_tac info kont gl =
     let open Proofview in
     let env = Goal.env gl in
     let sigma = Goal.sigma gl in
-    let s = Sigma.to_evar_map sigma in
     let decl = Tacmach.New.pf_last_hyp gl in
     let hint =
-      make_resolve_hyp env s (Hint_db.transparent_state info.search_hints)
+      make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints)
                        (true,false,false) info.search_only_classes empty_hint_info decl in
-    let ldb = Hint_db.add_list env s hint info.search_hints in
+    let ldb = Hint_db.add_list env sigma hint info.search_hints in
     let info' =
       { info with search_hints = ldb; last_tac = lazy (str"intro");
         search_depth = 1 :: 1 :: info.search_depth }
@@ -1238,7 +1234,7 @@ module Search = struct
 
   let intro info kont =
     Proofview.tclBIND Tactics.intro
-     (fun _ -> Proofview.Goal.enter { enter = fun gl -> intro_tac info kont gl })
+     (fun _ -> Proofview.Goal.enter (fun gl -> intro_tac info kont gl))
 
   let rec search_tac hints limit depth =
     let kont info =
@@ -1271,8 +1267,8 @@ module Search = struct
     let open Proofview in
     let tac sigma gls i =
       Goal.enter
-        { enter = fun gl ->
-          search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl }
+        begin fun gl ->
+          search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
     in
       Proofview.Unsafe.tclGETGOALS >>= fun gls ->
       Proofview.tclEVARMAP >>= fun sigma ->
@@ -1627,13 +1623,13 @@ let is_ground c =
 
 let autoapply c i =
   let open Proofview.Notations in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let flags = auto_unif_flags Evar.Set.empty
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
   let cty = Tacmach.New.pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-    (unify_e_resolve false flags).enter gl
+    unify_e_resolve false flags gl
                                  ((c,cty,Univ.ContextSet.empty),0,ce) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
-      Proofview.Unsafe.tclEVARS sigma) end }
+      Proofview.Unsafe.tclEVARS sigma) end
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 5e7090ded1..83c2be4106 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -25,22 +25,20 @@ let mk_absurd_proof coq_not t =
     mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let sigma = Sigma.to_evar_map sigma in
     let j = Retyping.get_judgment_of env sigma c in
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
-    let tac =
+    Proofview.Unsafe.tclEVARS sigma <*>
     Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot ->
     Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
       elim_type coqfalse;
       Simple.apply (mk_absurd_proof coqnot t)
-    ] in
-    Sigma.Unsafe.of_pair (tac, sigma)
-  end }
+    ]
+  end
 
 let absurd c = absurd c
 
@@ -54,13 +52,13 @@ let filter_hyp f tac =
     | [] -> Proofview.tclZERO Not_found
     | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
     | _::rest -> seek rest in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek hyps
-  end }
+  end
 
 let contradiction_context =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
@@ -89,11 +87,11 @@ let contradiction_context =
                | None ->
                  Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
 	      (Proofview.tclORELSE
-                 (Proofview.Goal.enter { enter = begin fun gl ->
+                 (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 (e, info) -> match e with
 	           | Not_found -> seek_neg rest
                    | e -> Proofview.tclZERO ~info e
@@ -102,7 +100,7 @@ let contradiction_context =
     in
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     seek_neg hyps
-  end }
+  end
 
 let is_negation_of env sigma typ t =
   match EConstr.kind sigma (whd_all env sigma t) with
@@ -111,7 +109,7 @@ let is_negation_of env sigma typ t =
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
@@ -134,7 +132,7 @@ let contradiction_term (c,lbind as cl) =
           | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
           | e -> Proofview.tclZERO ~info e
         end
-  end }
+  end
 
 let contradiction = function
   | None -> Tacticals.New.tclTHEN intros contradiction_context
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 986f531397..bae3344612 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -30,27 +30,27 @@ open Proofview.Notations
 let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma t1 || occur_existential sigma t2 then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
-  end }
+  end
 
 let assumption id = e_give_exact (mkVar id)
 
 let e_assumption =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
-  end }
+  end
 
 let registered_e_assumption =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
               (Tacmach.New.pf_ids_of_hyps gl))
-  end }
+  end
 
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
@@ -93,7 +93,7 @@ let out_term = function
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
   let map c =
-    let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
+    let (sigma, c) = c (pf_env gl) (project gl) in
     let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
     out_term c
   in
@@ -112,13 +112,13 @@ open Auto
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
         (Tactics.Simple.eapply c)
-    end }
+    end
 
 let hintmap_of sigma secvars hdc concl =
   match hdc with
@@ -130,20 +130,20 @@ let hintmap_of sigma secvars hdc concl =
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let clenv', c = connect_hint_clenv poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
-  end }
+  end
 
 let rec e_trivial_fail_db db_list local_db =
-  let next = Proofview.Goal.enter { enter = begin fun gl ->
+  let next = Proofview.Goal.enter begin fun gl ->
     let d = Tacmach.New.pf_last_hyp gl in
     let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
     e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
-  end } in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  end in
+  Proofview.Goal.enter begin fun gl ->
   let secvars = compute_secvars gl in
   let tacl =
     registered_e_assumption ::
@@ -151,7 +151,7 @@ let rec e_trivial_fail_db db_list local_db =
     (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
-  end }
+  end
 
 and e_my_find_search sigma db_list local_db secvars hdc concl =
   let hint_of_db = hintmap_of sigma secvars hdc concl in
@@ -497,7 +497,7 @@ let unfold_head env sigma (ids, csts) c =
   in aux c
 
 let autounfold_one db cl =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
@@ -517,4 +517,4 @@ let autounfold_one db cl =
       | Some hyp -> change_in_hyp None (make_change_arg c') hyp
       | None -> convert_concl_no_check c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
-  end }
+  end
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 855cb206fe..13d64b8e3f 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -77,7 +77,7 @@ let tmphyp_name = Id.of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let sigma = project gl in
   let typc = type_of c in
@@ -87,7 +87,7 @@ let general_decompose recognizer c =
 	    (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma))
 	      (fun id -> clear [id])));
        exact_no_check c ]
-  end }
+  end
 
 let head_in indl t gl =
   let env = Proofview.Goal.env gl in
@@ -101,10 +101,10 @@ let head_in indl t gl =
   with Not_found -> false
 
 let decompose_these c l =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
   general_decompose (fun sigma (_,t) -> head_in indl t gl) c
-  end }
+  end
 
 let decompose_and c =
   general_decompose
@@ -132,7 +132,7 @@ let induction_trailer abs_i abs_j bargs =
     (tclDO (abs_j - abs_i) intro)
     (onLastHypId
        (fun id ->
-          Proofview.Goal.enter { enter = begin fun gl ->
+          Proofview.Goal.enter begin fun gl ->
 	  let idty = pf_unsafe_type_of gl (mkVar id) in
 	  let fvty = global_vars (pf_env gl) (project gl) idty in
 	  let possible_bring_hyps =
@@ -150,11 +150,11 @@ let induction_trailer abs_i abs_j bargs =
           let ids = List.rev (ids_of_named_context hyps) in
 	  (tclTHENLIST
             [revert ids; simple_elimination (mkVar id)])
-          end }
+          end
           ))
 
 let double_ind h1 h2 =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let abs_i = depth_of_quantified_hypothesis true h1 gl in
   let abs_j = depth_of_quantified_hypothesis true h2 gl in
   let abs =
@@ -167,7 +167,7 @@ let double_ind h1 h2 =
        	(fun id ->
            elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
-  end }
+  end
 
 let h_double_induction = double_ind
 
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 93073fdc7e..466b1350d9 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -18,7 +18,6 @@ open Indrec
 open Declarations
 open Typeops
 open Ind_tables
-open Sigma.Notations
 
 (* Induction/recursion schemes *)
 
@@ -109,10 +108,10 @@ let rec_dep_scheme_kind_from_type =
 
 let build_case_analysis_scheme_in_type dep sort ind =
   let env = Global.env () in
-  let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in
-  let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in
-  let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep sort in
-    c, Evd.evar_universe_context (Sigma.to_evar_map sigma)
+  let sigma = Evd.from_env env in
+  let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in
+  let (sigma, c) = build_case_analysis_scheme env sigma indu dep sort in
+    c, Evd.evar_universe_context sigma
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 48ce52f092..0cee4b6edb 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -23,7 +23,6 @@ open Tacticals.New
 open Auto
 open Constr_matching
 open Misctypes
-open Tactypes
 open Hipattern
 open Proofview.Notations
 open Tacmach.New
@@ -66,22 +65,20 @@ let choose_noteq eqonleft =
   else
     left_with_bindings false Misctypes.NoBindings
 
-open Sigma.Notations
-
 (* A surgical generalize which selects the right occurrences by hand *)
 (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
 
 let generalize_right mk typ c1 c2 =
-  Proofview.Goal.enter { Proofview.Goal.enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
-  Refine.refine ~unsafe:true { Sigma.run = begin fun sigma ->
+  Refine.refine ~unsafe:true begin fun sigma ->
     let na = Name (next_name_away_with_default "x" Anonymous (Termops.ids_of_context env)) in
     let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
-    let Sigma (x, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
-    Sigma (mkApp (x, [|c2|]), sigma, p)
-  end }
-  end }
+    let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+    (sigma, mkApp (x, [|c2|]))
+  end
+  end
 
 let mkBranches (eqonleft,mk,c1,c2,typ) =
   tclTHENLIST
@@ -93,7 +90,7 @@ let mkBranches (eqonleft,mk,c1,c2,typ) =
      intros]
 
 let discrHyp id =
-  let c = { delayed = fun env sigma -> Sigma.here (mkVar id, NoBindings) sigma } in
+  let c env sigma = (sigma, (mkVar id, NoBindings)) in
   let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
@@ -138,7 +135,7 @@ let eqCase tac =
   tclTHEN intro (onLastHypId tac)
 
 let injHyp id =
-  let c = { delayed = fun env sigma -> Sigma.here (mkVar id, NoBindings) sigma } in
+  let c env sigma = (sigma, (mkVar id, NoBindings)) in
   let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
@@ -189,7 +186,7 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
     intros_reflexivity;
   ]
 | a1 :: largs, a2 :: rargs ->
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let rectype = pf_unsafe_type_of gl a1 in
   let decide = mk rectype a1 a2 in
   let tac hyp = solveArg (hyp :: hyps) eqonleft mk largs rargs in
@@ -197,13 +194,13 @@ let rec solveArg hyps eqonleft mk largs rargs = match largs, rargs with
     if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
     else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
   (tclTHENS (elim_type decide) subtacs)
-  end }
+  end
 | _ -> invalid_arg "List.fold_right2"
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
         match_eqdec sigma concl >>= fun (eqonleft,mk,lhs,rhs,_) ->
@@ -212,8 +209,9 @@ let solveEqBranch rectype =
           let getargs l = List.skipn nparams (snd (decompose_app sigma l)) in
           let rargs   = getargs rhs
           and largs   = getargs lhs in
+
           solveArg [] eqonleft mk largs rargs
-      end }
+      end
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
@@ -229,7 +227,7 @@ let hd_app sigma c = match EConstr.kind sigma c with
 let decideGralEquality =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
         match_eqdec sigma concl >>= fun (eqonleft,mk,c1,c2,typ as data) ->
@@ -241,7 +239,7 @@ let decideGralEquality =
           (tclTHEN
              (mkBranches data)
              (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
-      end }
+      end
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure ->
@@ -252,10 +250,10 @@ let decideGralEquality =
 let decideEqualityGoal = tclTHEN intros decideGralEquality
 
 let decideEquality rectype ops =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let decide = mkGenDecideEqGoal rectype ops gl in
   (tclTHENS (cut decide) [default_auto;decideEqualityGoal])
-  end }
+  end
 
 
 (* The tactic Compare *)
@@ -264,7 +262,7 @@ let compare c1 c2 =
   pf_constr_of_global (build_coq_sumbool ()) >>= fun opc ->
   pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc ->
   pf_constr_of_global (build_coq_not ()) >>= fun notc ->
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let rectype = pf_unsafe_type_of gl c1 in
   let ops = (opc,eqc,notc) in
   let decide = mkDecideEqGoal true ops rectype c1 c2 in
@@ -272,4 +270,4 @@ let compare c1 c2 =
             [(tclTHEN  intro
              (tclTHEN (onLastHyp simplest_case) clear_last));
              decideEquality rectype ops])
-  end }
+  end
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 507ff10eea..efcefcf16a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -57,7 +57,6 @@ open Namegen
 open Inductiveops
 open Ind_tables
 open Indrec
-open Sigma.Notations
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -656,10 +655,10 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
 (**********************************************************************)
  
 let build_r2l_rew_scheme dep env ind k =
-  let sigma = Sigma.Unsafe.of_evar_map (Evd.from_env env) in
-  let Sigma (indu, sigma, _) = Sigma.fresh_inductive_instance env sigma ind in
-  let Sigma (c, sigma, _) = build_case_analysis_scheme env sigma indu dep k in
-    c, Evd.evar_universe_context (Sigma.to_evar_map sigma)
+  let sigma = Evd.from_env env in
+  let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind in
+  let (sigma, c) = build_case_analysis_scheme env sigma indu dep k in
+    c, Evd.evar_universe_context sigma
 
 let build_l2r_rew_scheme = build_l2r_rew_scheme
 let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d64cc38eff..05c5cd5ec1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,7 +40,6 @@ open Eqschemes
 open Locus
 open Locusops
 open Misctypes
-open Sigma.Notations
 open Proofview.Notations
 open Unification
 open Context.Named.Declaration
@@ -254,16 +253,16 @@ let rewrite_keyed_unif_flags = {
 }
 
 let rewrite_elim with_evars frzevars cls c e =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let flags = if Unification.is_keyed_unification ()
 	      then rewrite_keyed_unif_flags else rewrite_conv_closed_unif_flags in
   let flags = make_flags frzevars (Tacmach.New.project gl) flags c in
   general_elim_clause with_evars flags cls c e
-  end }
+  end
 
 let tclNOTSAMEGOAL tac =
   let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
     let sigma = project gl in
     let ev = goal gl in
     tac >>= fun () ->
@@ -278,7 +277,7 @@ let tclNOTSAMEGOAL tac =
       tclZEROMSG (str"Tactic generated a subgoal identical to the original goal.")
     else
       Proofview.tclUNIT ()
-  end }
+  end
 
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars frzevars cls rew elim =
@@ -313,7 +312,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
          (general_elim_clause with_evars frzevars cls c elim))
       tac
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let instantiate_lemma concl =
       if not all then instantiate_lemma gl c t l l2r concl
       else instantiate_lemma_all frzevars gl c t l l2r concl
@@ -325,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
     else tclMAP try_clause cs
-  end }
+  end
 
 (* The next function decides in particular whether to try a regular
   rewrite or a generalized rewrite.
@@ -387,9 +386,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-      let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+      let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
       let elim = EConstr.of_constr elim in
-      Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
+      (sigma, (elim, Safe_typing.empty_private_constants))
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
@@ -407,11 +406,11 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   | Ind (ind,u) -> 
       let c, eff = find_scheme scheme_name ind in 
       (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
-      let Sigma (elim, sigma, p) =
-	Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+      let (sigma, elim) =
+	fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
       in
       let elim = EConstr.of_constr elim in
-      Sigma ((elim, eff), sigma, p)
+      (sigma, (elim, eff))
   | _ -> assert false
 
 let type_of_clause cls gl = match cls with
@@ -419,21 +418,19 @@ let type_of_clause cls gl = match cls with
   | Some id -> 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.s_enter { s_enter = begin fun gl ->
-  let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+  Proofview.Goal.enter begin fun gl ->
+  let evd = Proofview.Goal.sigma gl in
   let isatomic = isProd evd (whd_zeta evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd c type_of_cls in
-  let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-  let tac =
+  let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+      Proofview.Unsafe.tclEVARS sigma <*>
       Proofview.tclEFFECTS 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); elimrename = None}
-  in
-  Sigma (tac, sigma, p)
-  end }
+  end
 
 let adjust_rewriting_direction args lft2rgt =
   match args with
@@ -456,7 +453,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
   if occs != AllOccurrences then (
     rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
   else
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
@@ -485,7 +482,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	            | None -> Proofview.tclZERO ~info e
             (* error "The provided term does not end with an equality or a declared rewrite relation." *)  
             end
-    end }
+    end
 
 let general_rewrite_ebindings =
   general_rewrite_ebindings_clause None
@@ -547,9 +544,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
             let ids_of_hyps = 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.enter { enter = begin fun gl ->
+          Proofview.Goal.enter begin fun gl ->
             do_hyps_atleastonce (ids gl)
-          end }
+          end
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
 	  tclIFTHENTRYELSEMUST
@@ -557,25 +554,25 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	   do_hyps
 
 let apply_special_clear_request clear_flag f =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try
-      let ((c, bl), sigma) = run_delayed env sigma f in
+      let (sigma, (c, bl)) = f env sigma in
       apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
     with
       e when catchable_exception e -> tclIDTAC
-  end }
+  end
 
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
-      let (c, sigma) = run_delayed env sigma f in
+      let (sigma, c) = f env sigma in
       tclWITHHOLES with_evars
         (general_rewrite_clause l2r with_evars ?tac c cl) sigma
-    end }
+    end
   in
   let rec doN l2r c = function
     | Precisely n when n <= 0 -> Proofview.tclUNIT ()
@@ -638,7 +635,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
       | None -> Proofview.tclUNIT ()
       | Some tac ->  tclCOMPLETE tac
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let get_type_of = pf_apply get_type_of gl in
   let t1 = get_type_of c1
   and t2 = get_type_of c2 in
@@ -664,7 +661,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
           tclTHEN (apply sym) assumption;
           try_prove_eq
          ])
-  end }
+  end
 
 let replace c1 c2 =
   replace_using_leibniz onConcl c2 c1 false false None
@@ -934,13 +931,9 @@ let build_selector env sigma dirn c ind special default =
   let ci = make_case_info env ind RegularStyle in
   sigma, mkCase (ci, p, c, Array.of_list brl)
 
-let new_global sigma gr =
-  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
-  in Sigma.to_evar_map sigma, c
-    
-let build_coq_False sigma = new_global sigma (build_coq_False ())
-let build_coq_True sigma = new_global sigma (build_coq_True ())
-let build_coq_I sigma = new_global sigma (build_coq_I ())
+let build_coq_False sigma = Evarutil.new_global sigma (build_coq_False ())
+let build_coq_True sigma = Evarutil.new_global sigma (build_coq_True ())
+let build_coq_I sigma = Evarutil.new_global sigma (build_coq_I ())
 
 let rec build_discriminator env sigma dirn c = function
   | [] ->
@@ -967,7 +960,7 @@ let rec build_discriminator env sigma dirn c = function
 *)
 
 let gen_absurdity id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
   if is_empty_type sigma hyp_typ
@@ -975,7 +968,7 @@ let gen_absurdity id =
     simplest_elim (mkVar id)
   else
     tclZEROMSG (str "Not the negation of an equality.")
-  end }
+  end
 
 (* Precondition: eq is leibniz equality
 
@@ -1032,17 +1025,17 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
 
 let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     match find_positions env sigma ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
 	discr_positions env sigma u eq_clause cpath dirn
-  end }
+  end
 
 let onEquality with_evars tac (c,lbindc) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
   let t = type_of c in
@@ -1054,10 +1047,10 @@ let onEquality with_evars tac (c,lbindc) =
   tclTHEN
     (Proofview.Unsafe.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
-  end }
+  end
 
 let onNegatedEquality with_evars tac =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -1068,7 +1061,7 @@ let onNegatedEquality with_evars tac =
             onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
         tclZEROMSG (str "Not a negated primitive equality.")
-  end }
+  end
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
@@ -1327,7 +1320,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
 let inject_if_homogenous_dependent_pair ty =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   try
     let sigma = Tacmach.New.project gl in
     let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
@@ -1367,7 +1360,7 @@ let inject_if_homogenous_dependent_pair ty =
           ])]
   with Exit ->
     Proofview.tclUNIT ()
-  end }
+  end
 
 (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it
    expands then only when the whdnf has a constructor of an inductive type
@@ -1451,7 +1444,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
   let post_tac c n =
     match ipats_style with
     | Some ipats ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let sigma = project gl in
         let destopt = match EConstr.kind sigma c with
         | Var id -> get_previous_hyp_position id gl
@@ -1464,7 +1457,7 @@ let injEq ?(old=false) with_evars clear_flag ipats =
           then intro_patterns_bound_to with_evars n destopt ipats
           else intro_patterns_to with_evars destopt ipats in
         tclTHEN clear_tac intro_tac
-      end }
+      end
     | None -> tclIDTAC in
   injEqThen post_tac l2r
 
@@ -1482,7 +1475,7 @@ let injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
       match find_positions env sigma ~no_discr:false t1 t2 with
@@ -1493,7 +1486,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 }
+  end
 
 let dEqThen with_evars ntac = function
   | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
@@ -1504,10 +1497,10 @@ let dEq with_evars =
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decomp_eq tac data (c, t) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
     decompEqThen (fun _ -> tac) data cl
-  end }
+  end
 
 let _ = declare_intro_decomp_eq intro_decomp_eq
 
@@ -1558,7 +1551,6 @@ let decomp_tuple_term env sigma c t =
   in decomprec (mkRel 1) c t
 
 let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
-  let sigma = Sigma.to_evar_map sigma in
   let typ = get_type_of env sigma dep_pair1 in
   (* We find all possible decompositions *)
   let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
@@ -1583,7 +1575,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   (* Retype to get universes right *)
   let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
-  Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
+  (sigma, (body, expected_goal))
 
 (* Like "replace" but decompose dependent equalities                      *)
 (* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *)
@@ -1591,42 +1583,38 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* on for further iterated sigma-tuples                                   *)
 
 let cutSubstInConcl l2r eqn =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_concl gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
-  let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let tac =
-  tclTHENFIRST
+  let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
+  tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (tclTHENFIRST
     (tclTHENLIST [
        (change_concl typ); (* Put in pattern form *)
        (replace_core onConcl l2r eqn)
     ])
-    (change_concl expected) (* Put in normalized form *)
-  in
-  Sigma (tac, sigma, p)
-  end }
+    (change_concl expected)) (* Put in normalized form *)
+  end
 
 let cutSubstInHyp l2r eqn id =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
   let typ = pf_get_hyp_typ id gl in
   let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
-  let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
-  let tac =
-    tclTHENFIRST
+  let (sigma, (typ, expected)) = subst_tuple_term env sigma e1 e2 typ in
+  tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (tclTHENFIRST
     (tclTHENLIST [
        (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
-  in
-  Sigma (tac, sigma, p)
-  end }
+    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)))
+  end
 
 let try_rewrite tac =
   Proofview.tclORELSE tac begin function (e, info) -> match e with
@@ -1648,11 +1636,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let eq = pf_apply get_type_of gl c in
   tclTHENS (cutSubstClause l2r eq cls)
     [Proofview.tclUNIT (); exact_no_check c]
-  end }
+  end
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
 let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1713,7 +1701,7 @@ let is_eq_x gl x d =
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
@@ -1742,13 +1730,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       else
        [Proofview.tclUNIT ()]) @
      [tclTRY (clear [x; hyp])])
-  end }
+  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.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let decl = pf_get_hyp x gl in
     (* If x has a body, simply replace x with body and clear x *)
@@ -1765,7 +1753,7 @@ let subst_one_var dep_proof_ok x =
 	       str".")
         with FoundHyp res -> res in
       subst_one dep_proof_ok x res
-  end }
+  end
 
 let subst_gen dep_proof_ok ids =
   tclMAP (subst_one_var dep_proof_ok) ids
@@ -1818,7 +1806,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
 
   (* Second step: treat equations *)
   let process hyp =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
@@ -1834,19 +1822,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
-    end }
+    end
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let ids = find_equations gl in
     tclMAP process ids
-  end }
+  end
 
   else
 
 (* Old implementation, not able to manage configurations like a=b, a=t,
    or situations like "a = S b, b = S a", or also accidentally unfolding
    let-ins *)
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let find_eq_data_decompose = find_eq_data_decompose gl in
   let test (_,c) =
@@ -1865,7 +1853,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
   let ids = List.map_filter test hyps in
   let ids = List.uniquize ids in
   subst_gen flags.rewrite_dependent_proof ids
-  end }
+  end
 
 (* Rewrite the first assumption for which a condition holds
    and gives the direction of the rewrite *)
@@ -1902,11 +1890,10 @@ let rewrite_assumption_cond cond_eq_term cl =
 	  with | Failure _ | UserError _ -> arec rest gl
 	end
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
-    let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
+  Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps gl in
     arec hyps gl
-  end }
+  end
 
 (* Generalize "subst x" to substitution of subterm appearing as an
    equation in the context, but not clearing the hypothesis *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 70e62eabac..773abb9f0c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -22,7 +22,6 @@ open Namegen
 open Libnames
 open Smartlocate
 open Misctypes
-open Tactypes
 open Termops
 open Inductiveops
 open Typing
@@ -34,7 +33,6 @@ open Pfedit
 open Tacred
 open Printer
 open Vernacexpr
-open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
 
@@ -1363,11 +1361,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
   Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
-  let map c =
-    let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (c, sigma, _) = c.delayed env sigma in
-    (Sigma.to_evar_map sigma, c)
-  in
+  let map c = c env sigma in
   let lems = List.map map lems in
   let sign = EConstr.named_context env in
   let ts = match ts with
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 9110830aae..a1d986544a 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -120,11 +120,11 @@ val match_with_equation:
 
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
@@ -145,7 +145,7 @@ val is_matching_sigma : evar_map -> constr -> bool
 val match_eqdec : evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
+val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
 val is_matching_not : evar_map -> constr -> bool
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b951e7ceba..ec038f638e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -25,7 +25,6 @@ open Tactics
 open Elim
 open Equality
 open Misctypes
-open Sigma.Notations
 open Proofview.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -272,14 +271,14 @@ Nota: with Inversion_clear, only four useless hypotheses
 
 let generalizeRewriteIntros as_mode tac depids id =
   Proofview.tclENV >>= fun env ->
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let dids = dependent_hyps env id depids gl in
   let reintros = if as_mode then intros_replacing else intros_possibly_replacing in
   (tclTHENLIST
     [bring_hyps dids; tac;
      (* may actually fail to replace if dependent in a previous eq *)
      reintros (ids_of_named_context dids)])
-  end }
+  end
 
 let error_too_many_names pats =
   let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in
@@ -287,7 +286,7 @@ let error_too_many_names pats =
   tclZEROMSG ?loc (
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
-    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed env Evd.empty c))))) pats ++
+    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
     str ".")
 
 let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
@@ -341,7 +340,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
   in
   let substHypIfVariable tac id =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let sigma = project gl in
     (** We only look at the type of hypothesis "id" *)
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
@@ -350,7 +349,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
     | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2
     | _ -> tac id
-    end }
+    end
   in
   let deq_trailer id clear_flag _ neqns =
     assert (clear_flag == None);
@@ -377,7 +376,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     id
 
 let nLastDecls i tac =
-  Proofview.Goal.enter { enter = begin fun gl -> tac (nLastDecls gl i) end }
+  Proofview.Goal.enter begin fun gl -> tac (nLastDecls gl i) end
 
 (* Introduction of the equations on arguments
    othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -385,7 +384,7 @@ let nLastDecls i tac =
      Some thin: the equations are rewritten, and cleared if thin is true *)
 
 let rewrite_equations as_mode othin neqns names ba =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
   let first_eq = ref MoveLast in
   let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in
@@ -418,7 +417,7 @@ let rewrite_equations as_mode othin neqns names ba =
              [tclDO neqns intro;
               bring_hyps nodepids;
               clear (ids_of_named_context nodepids)])
-  end }
+  end
 
 let interp_inversion_kind = function
   | SimpleInversion -> None
@@ -435,9 +434,8 @@ let rewrite_equations_tac as_mode othin id neqns names ba =
     tac
 
 let raw_inversion inv_kind id status names =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let sigma = Sigma.to_evar_map sigma in
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
@@ -462,11 +460,11 @@ let raw_inversion inv_kind id status names =
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
-      Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
+      Refine.refine (fun h -> (h, prf))
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
-    let tac =
+    tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (tclTHENS
         (assert_before Anonymous cut_concl)
         [case_tac names
@@ -474,9 +472,7 @@ let raw_inversion inv_kind id status names =
                (rewrite_equations_tac as_mode inv_kind id neqns))
             (Some elim_predicate) ind (c,t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
-    in
-    Sigma.Unsafe.of_pair (tac, sigma)
-  end }
+  end
 
 (* Error messages of the inversion tactics *)
 let wrap_inv_error id = function (e, info) -> match e with
@@ -516,13 +512,13 @@ 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.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
     let nb_prod_init = nb_prod sigma concl in
     let intros_replace_ids =
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let concl = pf_concl gl in
         let sigma = project gl in
         let nb_of_new_hyp =
@@ -532,7 +528,7 @@ let invIn k names ids id =
           intros_replacing ids
         else
           tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)
-      end }
+      end
     in
     Proofview.tclORELSE
       (tclTHENLIST
@@ -540,7 +536,7 @@ let invIn k names ids id =
           inversion k NoDep names id;
           intros_replace_ids])
       (wrap_inv_error id)
-  end }
+  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 83f3da30a9..87d815fc81 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -27,7 +27,6 @@ open Declare
 open Tacticals.New
 open Tactics
 open Decl_kinds
-open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -261,7 +260,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
 (* ================================= *)
 
 let lemInv id c =
-  Proofview.Goal.enter { enter = begin fun gls ->
+  Proofview.Goal.enter begin fun gls ->
   try
     let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
@@ -274,12 +273,12 @@ let lemInv id c =
 	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
 	      pr_leconstr_env (pf_env gls) (project gls) c)
-  end }
+  end
 
 let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
 
 let lemInvIn id c ids =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
     let intros_replace_ids =
       let concl = Proofview.Goal.concl gl in
@@ -292,7 +291,7 @@ let lemInvIn id c ids =
     in
     ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
         (intros_replace_ids)))
-  end }
+  end
 
 let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index a7eadc3c3e..aa574e41c5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -17,7 +17,6 @@ open Declarations
 open Tacmach
 open Clenv
 open Tactypes
-open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
 
@@ -511,12 +510,12 @@ module New = struct
         Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclDELAYEDWITHHOLES check x tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      let Sigma (x, sigma, _) = x.delayed env sigma in
-      tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
-    end }
+      let (sigma, x) = x env sigma in
+      tclWITHHOLES check (tac x) sigma
+    end
 
   let tclTIMEOUT n t =
     Proofview.tclOR
@@ -547,66 +546,66 @@ module New = struct
     mkVar (nthHypId m gl)
 
   let onNthHypId m tac =
-    Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end }
+    Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end 
   let onNthHyp m tac =
-    Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end }
+    Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
 
   let onLastHypId = onNthHypId 1
   let onLastHyp   = onNthHyp 1
 
   let onNthDecl m tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       Proofview.tclUNIT (nthDecl m gl) >>= tac
-    end }
+    end
   let onLastDecl  = onNthDecl 1
 
   let ifOnHyp pred tac1 tac2 id =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    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 }
+    end
 
-  let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end }
+  let onHyps find tac = Proofview.Goal.enter begin fun gl -> tac (find gl) end
 
   let afterHyp id tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
     let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
     tac rem
-    end }
+    end
 
   let fullGoal gl =
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     None :: List.map Option.make hyps
 
   let tryAllHyps tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let hyps = Tacmach.New.pf_ids_of_hyps gl in
     tclFIRST_PROGRESS_ON tac hyps
-    end }
+    end
   let tryAllHypsAndConcl tac =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       tclFIRST_PROGRESS_ON tac (fullGoal gl)
-    end }
+    end
 
   let onClause tac cl =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    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 }
+    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 ind (c, t) =
-    Proofview.Goal.enter { enter = begin fun gl ->
-    let sigma, elim = (mk_elim ind).enter gl in
+    Proofview.Goal.enter begin fun gl ->
+    let sigma, elim = mk_elim ind gl in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Proofview.Goal.enter { enter = begin fun gl ->
+    (Proofview.Goal.enter begin fun gl ->
     let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
     let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
@@ -655,7 +654,7 @@ module New = struct
     Proofview.tclTHEN
       (Clenvtac.clenv_refine false clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
-    end }) end }
+    end) end
 
   let elimination_sort_of_goal gl =
     (** Retyping will expand evars anyway. *)
@@ -673,29 +672,29 @@ module New = struct
 
   (* computing the case/elim combinators *)
 
-  let gl_make_elim ind = { enter = begin fun gl ->
+  let gl_make_elim ind = begin fun gl ->
     let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
     let (sigma, c) = pf_apply Evd.fresh_global gl gr in
     (sigma, EConstr.of_constr c)
-  end }
+  end
 
-  let gl_make_case_dep (ind, u) = { enter = begin fun gl ->
-    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+  let gl_make_case_dep (ind, u) = begin fun gl ->
+    let sigma = project gl in
     let u = EInstance.kind (project gl) u in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
+    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
       (elimination_sort_of_goal gl)
     in
-    (Sigma.to_evar_map sigma, EConstr.of_constr r)
-  end }
+    (sigma, EConstr.of_constr r)
+  end
 
-  let gl_make_case_nodep (ind, u) = { enter = begin fun gl ->
-    let sigma = Sigma.Unsafe.of_evar_map (project gl) in
-    let u = EInstance.kind (project gl) u in
-    let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
+  let gl_make_case_nodep (ind, u) = begin fun gl ->
+    let sigma = project gl in
+    let u = EInstance.kind sigma u in
+    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
       (elimination_sort_of_goal gl)
     in
-    (Sigma.to_evar_map sigma, EConstr.of_constr r)
-  end }
+    (sigma, EConstr.of_constr r)
+  end
 
   let make_elim_branch_assumptions ba hyps =
     let assums =
@@ -704,19 +703,19 @@ module New = struct
     { ba = ba; assums = assums }
 
   let elim_on_ba tac ba =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
     tac branches
-    end }
+    end
 
   let case_on_ba tac ba = 
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
     tac branches
-    end }
+    end
 
   let elimination_then tac c =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
@@ -724,7 +723,7 @@ module New = struct
       | Some _ -> false,gl_make_case_dep
     in
     general_elim_then_using mkelim isrec None tac None ind (c, t)
-    end }
+    end
 
   let case_then_using =
     general_elim_then_using gl_make_case_dep false
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 96270f748e..9603212de6 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -225,7 +225,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : ('a, 'r) Proofview.Goal.t -> int -> named_context
+  val nLastDecls  : 'a Proofview.Goal.t -> int -> named_context
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
@@ -236,7 +236,7 @@ module New : sig
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `LZ ], named_context) Proofview.Goal.enter ->
+  val onHyps      : ([ `LZ ] Proofview.Goal.t -> named_context) ->
                     (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
@@ -244,9 +244,9 @@ module New : sig
   val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
   val onClause   : (identifier option -> unit tactic) -> clause -> unit tactic
 
-  val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family
-  val elimination_sort_of_hyp  : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family
-  val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_hyp  : Id.t -> 'a Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family
 
   val elimination_then :
     (branch_args -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a93a86d3a3..b553f316c2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,9 +43,7 @@ open Unification
 open Locus
 open Locusops
 open Misctypes
-open Tactypes
 open Proofview.Notations
-open Sigma.Notations
 open Context.Named.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -55,7 +53,7 @@ let inj_with_occurrences e = (AllOccurrences,e)
 
 let typ_of env sigma c =
   let open Retyping in
-  try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c
+  try get_type_of ~lax:true env sigma c
   with RetypeError e ->
     user_err (print_retype_error e)
 
@@ -165,18 +163,18 @@ let _ =
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
 let unsafe_intro env store decl b =
-  Refine.refine ~unsafe:true { run = begin fun sigma ->
+  Refine.refine ~unsafe:true begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
     let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
-    let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
-    Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p)
-  end }
+    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+    (sigma, mkNamedLambda_or_LetIn decl ev)
+  end
 
 let introduction ?(check=true) id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
@@ -192,49 +190,48 @@ let introduction ?(check=true) id =
     | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
     | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
     | _ -> raise (RefinerError IntroNeedsProduct)
-  end }
+  end
 
 let refine          = Tacmach.refine
 let error msg = CErrors.user_err Pp.(str msg)
 
 let convert_concl ?(check=true) ty k =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
     let conclty = Proofview.Goal.concl gl in
-    Refine.refine ~unsafe:true { run = begin fun sigma ->
-      let Sigma ((), sigma, p) =
+    Refine.refine ~unsafe:true begin fun sigma ->
+      let sigma =
         if check then begin
-          let sigma = Sigma.to_evar_map sigma in
           ignore (Typing.unsafe_type_of env sigma ty);
           let sigma,b = Reductionops.infer_conv env sigma ty conclty in
           if not b then error "Not convertible.";
-          Sigma.Unsafe.of_pair ((), sigma)
-        end else Sigma.here () sigma in
-      let Sigma (x, sigma, q) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+          sigma
+        end else sigma in
+      let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
-      Sigma (ans, sigma, p +> q)
-    end }
-  end }
+      (sigma, ans)
+    end
+  end
 
 let convert_hyp ?(check=true) d =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
     let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
-    Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ~store ty
-    end }
-  end }
+    end
+  end
 
 let convert_concl_no_check = convert_concl ~check:false
 let convert_hyp_no_check = convert_hyp ~check:false
 
 let convert_gen pb x y =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     try
       let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
       if b then Proofview.Unsafe.tclEVARS sigma
@@ -242,7 +239,7 @@ let convert_gen pb x y =
     with (* Reduction.NotConvertible *) _ ->
       (** FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
-end }
+end
 
 let convert x y = convert_gen Reduction.CONV x y
 let convert_leq x y = convert_gen Reduction.CUMUL x y
@@ -282,7 +279,7 @@ let error_replacing_dependency env sigma id err =
 let clear_gen fail = function
 | [] -> Proofview.tclUNIT ()
 | ids ->
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let ids = List.fold_right Id.Set.add ids Id.Set.empty in
     (** clear_hyps_in_evi does not require nf terms *)
     let gl = Proofview.Goal.assume gl in
@@ -295,11 +292,11 @@ let clear_gen fail = function
       with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
     in
     let env = reset_with_named_context hyps env in
-    let tac = Refine.refine ~unsafe:true { run = fun sigma ->
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
+    (Refine.refine ~unsafe:true begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
-    } in
-    Sigma.Unsafe.of_pair (tac, !evdref)
-  end }
+    end)
+  end
 
 let clear ids = clear_gen error_clear_dependency ids
 let clear_for_replacing ids = clear_gen error_replacing_dependency ids
@@ -318,7 +315,7 @@ let apply_clear_request clear_flag dft c =
 
 (* Moving hypotheses *)
 let move_hyp id dest =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
@@ -326,10 +323,10 @@ let move_hyp id dest =
     let sign = named_context_val env in
     let sign' = move_hyp_in_named_context sigma id dest sign in
     let env = reset_with_named_context sign' env in
-    Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ~store ty
-    end }
-  end }
+    end
+  end
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
@@ -348,7 +345,7 @@ let rename_hyp repl =
   match dom with
   | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
   | Some (src, dst) ->
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let gl = Proofview.Goal.assume gl in
       let hyps = Proofview.Goal.hyps gl in
       let concl = Proofview.Goal.concl gl in
@@ -380,10 +377,10 @@ let rename_hyp repl =
       let nconcl = subst concl in
       let nctx = val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
-      Refine.refine ~unsafe:true { run = begin fun sigma ->
+      Refine.refine ~unsafe:true begin fun sigma ->
         Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
-      end }
-    end }
+      end
+    end
 
 (**************************************************************)
 (*          Fresh names                                       *)
@@ -447,7 +444,7 @@ let find_name mayrepl decl naming gl = match naming with
 
 let assert_before_then_gen b naming t tac =
   let open Context.Rel.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
     Tacticals.New.tclTHENLAST
       (Proofview.V82.tactic
@@ -456,7 +453,7 @@ let assert_before_then_gen b naming t tac =
            with Evarutil.ClearDependencyError (id,err) ->
              error_replacing_dependency (pf_env gl) (project gl) id err))
       (tac id)
-  end }
+  end
 
 let assert_before_gen b naming t =
   assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ())
@@ -466,7 +463,7 @@ let assert_before_replacing id = assert_before_gen true (NamingMustBe (Loc.tag i
 
 let assert_after_then_gen b naming t tac =
   let open Context.Rel.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let id = find_name b (LocalAssum (Anonymous,t)) naming gl in
     Tacticals.New.tclTHENFIRST
       (Proofview.V82.tactic
@@ -475,7 +472,7 @@ let assert_after_then_gen b naming t tac =
            with Evarutil.ClearDependencyError (id,err) ->
              error_replacing_dependency (pf_env gl) (project gl) id err))
       (tac id)
-  end }
+  end
 
 let assert_after_gen b naming t =
   assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ()))
@@ -487,13 +484,12 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (Loc.tag id)
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
 
-let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma =
-fun env sigma p -> function
-| [] -> Sigma ([], sigma, p)
+let rec mk_holes env sigma = function
+| [] -> (sigma, [])
 | arg :: rem ->
-  let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in
-  let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in
-  Sigma (arg :: rem, sigma, r)
+  let (sigma, arg) = Evarutil.new_evar env sigma arg in
+  let (sigma, rem) = mk_holes env sigma rem in
+  (sigma, arg :: rem)
 
 let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) with
 | Prod (na, c1, b) ->
@@ -511,7 +507,7 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
 | _ -> error "Not enough products."
 
 (* Refine as a fixpoint *)
-let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl ->
+let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
@@ -531,8 +527,8 @@ let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl ->
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
-  Refine.refine { run = begin fun sigma ->
-    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in
+  Refine.refine begin fun sigma ->
+    let (sigma, evs) = mk_holes nenv sigma (List.map pi3 all) in
     let ids = List.map pi1 all in
     let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
     let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
@@ -540,17 +536,17 @@ let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl ->
     let typarray = Array.of_list (List.map pi3 all) in
     let bodies = Array.of_list evs in
     let oterm = mkFix ((indxs,0),(funnames,typarray,bodies)) in
-    Sigma (oterm, sigma, p)
-  end }
-end }
+    (sigma, oterm)
+  end
+end
 
 let fix ido n = match ido with
   | None ->
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let name = Pfedit.get_current_proof_name () in
       let id = new_fresh_id [] name gl in
       mutual_fix id n [] 0
-    end }
+    end
   | Some id ->
     mutual_fix id n [] 0
 
@@ -567,7 +563,7 @@ let rec check_is_mutcoind env sigma cl =
       error "All methods must construct elements in coinductive types."
 
 (* Refine as a cofixpoint *)
-let mutual_cofix f others j = Proofview.Goal.enter { enter = begin fun gl ->
+let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
@@ -583,25 +579,25 @@ let mutual_cofix f others j = Proofview.Goal.enter { enter = begin fun gl ->
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
-  Refine.refine { run = begin fun sigma ->
+  Refine.refine begin fun sigma ->
     let (ids, types) = List.split all in
-    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in
+    let (sigma, evs) = mk_holes nenv sigma types in
     let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
     let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
     let typarray = Array.of_list types in
     let bodies = Array.of_list evs in
     let oterm = mkCoFix (0, (funnames, typarray, bodies)) in
-    Sigma (oterm, sigma, p)
-  end }
-end }
+    (sigma, oterm)
+  end
+end
 
 let cofix ido = match ido with
   | None ->
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let name = Pfedit.get_current_proof_name () in
       let id = new_fresh_id [] name gl in
       mutual_cofix id [] 0
-    end }
+    end
   | Some id ->
       mutual_cofix id [] 0
 
@@ -693,14 +689,14 @@ let bind_red_expr_occurrences occs nbcl redexp =
    certain hypothesis *)
 
 let reduct_in_concl (redfun,sty) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
-  end }
+  end
 
 let reduct_in_hyp ?(check=false) redfun (id,where) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
-  end }
+  end
 
 let revert_cast (redfun,kind as r) =
   if kind == DEFAULTcast then (redfun,REVERTcast) else r
@@ -714,30 +710,32 @@ let reduct_option ?(check=false) redfun = function
 let pf_e_reduce_decl redfun where decl gl =
   let open Context.Named.Declaration in
   let sigma = Proofview.Goal.sigma gl in
-  let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in
+  let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
-    let Sigma (ty', sigma, p) = redfun sigma ty in
-    Sigma (LocalAssum (id, ty'), sigma, p)
+    let (sigma, ty') = redfun sigma ty in
+    (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
-      let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in
-      let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in
-      Sigma (LocalDef (id, b', ty'), sigma, p +> q)
+      let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in
+      let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in
+      (sigma, LocalDef (id, b', ty'))
 
 let e_reduct_in_concl ~check (redfun, sty) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
-    Sigma (convert_concl ~check c' sty, sigma, p)
-  end }
+    let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (convert_concl ~check c' sty)
+  end
 
 let e_reduct_in_hyp ?(check=false) redfun (id, where) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
-    Sigma (convert_hyp ~check decl', sigma, p)
-  end }
+  Proofview.Goal.enter begin fun gl ->
+    let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (convert_hyp ~check decl')
+  end
 
 let e_reduct_option ?(check=false) redfun = function
   | Some id -> e_reduct_in_hyp ~check (fst redfun) id
@@ -747,11 +745,12 @@ let e_reduct_option ?(check=false) redfun = function
     from conversions. *)
 
 let e_change_in_concl (redfun,sty) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
-    Sigma (convert_concl_no_check c sty, sigma, p)
-  end }
+    let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (convert_concl_no_check c sty)
+  end
 
 let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
   let open Context.Named.Declaration in
@@ -759,29 +758,29 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
 	user_err  (pr_id id ++ str " has no value.");
-    let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
-    Sigma (LocalAssum (id, ty'), sigma, p)
+    let (sigma, ty') = redfun false env sigma ty in
+    (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
-      let Sigma (b', sigma, p) =
-	if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma
+      let (sigma, b') =
+	if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
       in
-      let Sigma (ty', sigma, q) =
-	if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma
+      let (sigma, ty') =
+	if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
       in
-      Sigma (LocalDef (id,b',ty'), sigma, p +> q)
+      (sigma, LocalDef (id,b',ty'))
 
 let e_change_in_hyp redfun (id,where) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
-    let Sigma (c, sigma, p) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
-    Sigma (convert_hyp c, sigma, p)
-  end }
+    let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (convert_hyp c)
+  end
 
-type change_arg = Pattern.patvar_map -> EConstr.constr Sigma.run
+type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr
 
-let make_change_arg c pats =
-  { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma }
+let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
@@ -805,33 +804,30 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
     else sigma
 
 (* Now we introduce different instances of the previous tacticals *)
-let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c ->
-  let Sigma (t', sigma, p) = t.run sigma in
-  let sigma = Sigma.to_evar_map sigma in
+let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
+  let (sigma, t') = t sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
   if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
-  Sigma.Unsafe.of_pair (t', sigma)
-end }
+  (sigma, t')
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c ->
+let change_on_subterm cv_pb deep t where env sigma c =
   let mayneedglobalcheck = ref false in
-  let Sigma (c, sigma, p) = match where with
-  | None -> (change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty)).e_redfun env sigma c
+  let (sigma, c) = match where with
+  | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
   | Some occl ->
-      (e_contextually false occl
+      e_contextually false occl
         (fun subst ->
-          change_and_check Reduction.CONV mayneedglobalcheck true (t subst))).e_redfun
+          change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
         env sigma c in
   if !mayneedglobalcheck then
     begin
-      try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c)
+      try ignore (Typing.unsafe_type_of env sigma c)
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
     end;
-  Sigma (c, sigma, p)
-end }
+  (sigma, c)
 
 let change_in_concl occl t =
   e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
@@ -844,7 +840,7 @@ let change_option occl t = function
   | None -> change_in_concl occl t
 
 let change chg c cls =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
     Tacticals.New.tclMAP (function
     | OnHyp (id,occs,where) ->
@@ -852,7 +848,7 @@ let change chg c cls =
     | OnConcl occs ->
        change_option (bind_change_occurrences occs chg) c None)
     cls
-  end }
+  end
 
 let change_concl t = 
   change_in_concl None (make_change_arg t)
@@ -893,14 +889,14 @@ let reduce redexp cl =
     Pp.(hov 2 (Pputils.pr_red_expr pr str redexp))
   in
   Proofview.Trace.name_tactic trace begin
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
   let redexps = reduction_clause redexp cl' in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   Tacticals.New.tclMAP (fun (where,redexp) ->
     e_reduct_option ~check
       (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
-  end }
+  end
   end
 
 (* Unfolding occurrences of a constant *)
@@ -936,7 +932,7 @@ let build_intro_tac id dest tac = match dest with
 
 let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   let open Context.Rel.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     match EConstr.kind sigma concl with
@@ -962,7 +958,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
                 Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
-  end }
+  end
 
 let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
 let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false
@@ -1027,14 +1023,14 @@ let get_previous_hyp_position id gl =
   aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
 let intro_replacing id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let next_hyp = get_next_hyp_position id gl in
   Tacticals.New.tclTHENLIST [
     clear_for_replacing [id];
     introduction id;
     move_hyp id next_hyp;
   ]
-  end }
+  end
 
 (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to
    reintroduce y, y,' y''. Note that we have to clear y, y' and y''
@@ -1046,7 +1042,7 @@ let intro_replacing id =
 (* the behavior of inversion *)
 let intros_possibly_replacing ids =
   let suboptimal = true in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
     Tacticals.New.tclTHEN
       (Tacticals.New.tclMAP (fun id -> 
@@ -1055,16 +1051,16 @@ let intros_possibly_replacing ids =
       (Tacticals.New.tclMAP (fun (id,pos) ->
         Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
          posl)
-  end }
+  end
 
 (* This version assumes that replacement is actually possible *)
 let intros_replacing ids =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
     Tacticals.New.tclTHEN
       (clear_for_replacing ids)
       (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
-  end }
+  end
 
 (* User-level introduction tactics *)
 
@@ -1078,7 +1074,7 @@ let lookup_hypothesis_as_renamed_gen red h gl =
     match lookup_hypothesis_as_renamed env (Tacmach.New.project gl) ccl h with
       | None when red ->
         let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
-        let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in
+        let (_, c) = redfun env (Proofview.Goal.sigma gl) ccl in
         aux c
       | x -> x
   in
@@ -1108,10 +1104,10 @@ let depth_of_quantified_hypothesis red h gl =
 	  str".")
 
 let intros_until_gen red h =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let n = depth_of_quantified_hypothesis red h gl in
   Tacticals.New.tclDO n (if red then introf else intro)
-  end }
+  end
 
 let intros_until_id id = intros_until_gen false (NamedHyp id)
 let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
@@ -1120,10 +1116,10 @@ let intros_until = intros_until_gen true
 let intros_until_n = intros_until_n_gen true
 
 let tclCHECKVAR id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
     Proofview.tclUNIT ()
-  end }
+  end
 
 let try_intros_until_id_check id =
   Tacticals.New.tclORELSE (intros_until_id id) (tclCHECKVAR id)
@@ -1138,9 +1134,6 @@ let rec intros_move = function
       Tacticals.New.tclTHEN (intro_gen (NamingMustBe (Loc.tag hyp)) destopt false false)
 	(intros_move rest)
 
-let run_delayed env sigma c =
-  Sigma.run sigma { Sigma.run = fun sigma -> c.delayed env sigma }
-
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
@@ -1154,7 +1147,7 @@ let tactic_infer_flags with_evar = {
 
 let onOpenInductionArg env sigma tac = function
   | clear_flag,ElimOnConstr f ->
-      let (cbl, sigma') = run_delayed env sigma f in
+      let (sigma', cbl) = f env sigma in
       Tacticals.New.tclTHEN
         (Proofview.Unsafe.tclEVARS sigma')
         (tac clear_flag (sigma,cbl))
@@ -1163,18 +1156,18 @@ let onOpenInductionArg env sigma tac = function
         (intros_until_n n)
         (Tacticals.New.onLastHyp
            (fun c ->
-             Proofview.Goal.enter { enter = begin fun gl ->
+             Proofview.Goal.enter begin fun gl ->
              let sigma = Tacmach.New.project gl in
              tac clear_flag (sigma,(c,NoBindings))
-             end }))
+             end))
   | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
       Tacticals.New.tclTHEN
         (try_intros_until_id_check id)
-        (Proofview.Goal.enter { enter = begin fun gl ->
+        (Proofview.Goal.enter begin fun gl ->
          let sigma = Tacmach.New.project gl in
          tac clear_flag (sigma,(mkVar id,NoBindings))
-        end })
+        end)
 
 let onInductionArg tac = function
   | clear_flag,ElimOnConstr cbl ->
@@ -1195,11 +1188,10 @@ let map_destruction_arg f sigma = function
   | clear_flag,ElimOnIdent id as x -> (sigma,x)
 
 let finish_delayed_evar_resolution with_evars env sigma f =
-  let ((c, lbind), sigma') = run_delayed env sigma f in
-  let sigma' = Sigma.Unsafe.of_evar_map sigma' in
+  let (sigma', (c, lbind)) = f env sigma in
   let flags = tactic_infer_flags with_evars in
-  let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in
-  (Sigma.to_evar_map sigma', (c, lbind))
+  let (sigma', c) = finish_evar_resolution ~flags env sigma' (sigma,c) in
+  (sigma', (c, lbind))
 
 let with_no_bindings (c, lbind) =
   if lbind != NoBindings then error "'with' clause not supported here.";
@@ -1215,7 +1207,7 @@ let force_destruction_arg with_evars env sigma c =
 let normalize_cut = false
 
 let cut c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
@@ -1233,15 +1225,15 @@ let cut c =
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
-      Refine.refine ~unsafe:true { run = begin fun h ->
-        let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
-        let Sigma (x, h, q) = Evarutil.new_evar env h c in
+      Refine.refine ~unsafe:true begin fun h ->
+        let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
+        let (h, x) = Evarutil.new_evar env h c in
         let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
-        Sigma (f, h, p +> q)
-      end }
+        (h, f)
+      end
     else
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
-  end }
+  end
 
 let error_uninstantiated_metas t clenv =
   let t = EConstr.Unsafe.to_constr t in
@@ -1352,12 +1344,12 @@ let enforce_prop_bound_names rename tac =
             mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
         | _ -> assert false in
       let rename_branch i =
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
           let env = Proofview.Goal.env gl in
           let sigma = Tacmach.New.project gl in
           let t = Proofview.Goal.concl gl in
           change_concl (aux env sigma i t)
-        end } in
+        end in
       (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
         tac
         (Array.map rename_branch nn)
@@ -1372,7 +1364,7 @@ let rec contract_letin_in_lam_header sigma c =
 
 let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) 
     rename i (elim, elimty, bindings) indclause =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let elim = contract_letin_in_lam_header sigma elim in
@@ -1385,7 +1377,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
   enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags)
-  end }
+  end
 
 (*
  * Elimination tactic with bindings and using an arbitrary
@@ -1402,7 +1394,7 @@ type eliminator = {
 }
 
 let general_elim_clause_gen elimtac indclause elim =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let (elimc,lbindelimc) = elim.elimbody in
@@ -1410,10 +1402,10 @@ let general_elim_clause_gen elimtac indclause elim =
   let i =
     match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in
   elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
-  end }
+  end
 
 let general_elim with_evars clear_flag (c, lbindc) elim =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let ct = Retyping.get_type_of env sigma c in
@@ -1425,32 +1417,30 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   Tacticals.New.tclTHEN
     (general_elim_clause_gen elimtac indclause elim)
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
-  end }
+  end
 
 (* Case analysis tactics *)
 
 let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  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 t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
-  let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in
+  let t = Retyping.get_type_of env sigma c in
+  let (mind,_) = reduce_to_quantified_ind env sigma t in
   let sort = Tacticals.New.elimination_sort_of_goal gl in
-  let mind = on_snd (fun u -> EInstance.kind (Sigma.to_evar_map sigma) u) mind in
-  let Sigma (elim, sigma, p) =
-    if occur_term (Sigma.to_evar_map sigma) c concl then
+  let mind = on_snd (fun u -> EInstance.kind sigma u) mind in
+  let (sigma, elim) =
+    if occur_term sigma c concl then
       build_case_analysis_scheme env sigma mind true sort
     else
       build_case_analysis_scheme_default env sigma mind sort in
   let elim = EConstr.of_constr elim in
-  let tac =
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
   (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
     elimrename = Some (false, constructors_nrealdecls (fst mind))})
-  in
-  Sigma (tac, sigma, p)
-  end }
+  end
 
 let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
   Proofview.tclEVARMAP >>= fun sigma ->
@@ -1486,13 +1476,11 @@ let find_eliminator c gl =
 
 let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
-    (Proofview.Goal.s_enter { s_enter = begin fun gl ->
+    (Proofview.Goal.enter begin fun gl ->
       let sigma, elim = find_eliminator c gl in
-      let tac =
-	  (general_elim with_evars clear_flag cx elim)
-      in
-      Sigma.Unsafe.of_pair (tac, sigma)
-    end })
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+      (general_elim with_evars clear_flag cx elim)
+    end)
     begin function (e, info) -> match e with
       | IsNonrec ->
           (* For records, induction principles aren't there by default
@@ -1540,7 +1528,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
 
 let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) 
     id rename i (elim, elimty, bindings) indclause =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let elim = contract_letin_in_lam_header sigma elim in
@@ -1563,7 +1551,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id id sigma elimclause''
     (fun id -> Proofview.tclUNIT ())
-  end }
+  end
 
 let general_elim_clause with_evars flags id c e =
   let elim = match id with
@@ -1622,7 +1610,7 @@ let make_projection env sigma params cstr sign elim i n c u =
   in elim
 
 let descend_in_conjunctions avoid tac (err, info) c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   try
@@ -1641,14 +1629,13 @@ let descend_in_conjunctions avoid tac (err, info) c =
 	  try DefinedRecord (Recordops.lookup_projections ind)
 	  with Not_found ->
             let u = EInstance.kind sigma u in
-            let sigma = Sigma.Unsafe.of_evar_map sigma in
-	    let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in
+	    let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
 	    let elim = EConstr.of_constr elim in
 	    NotADefinedRecordUseScheme elim in
 	Tacticals.New.tclORELSE0
 	(Tacticals.New.tclFIRST
 	  (List.init n (fun i ->
-            Proofview.Goal.enter { enter = begin fun gl ->
+            Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
             let sigma = Tacmach.New.project gl in
 	    match make_projection env sigma params cstr sign elim i n c u with
@@ -1659,32 +1646,31 @@ let descend_in_conjunctions avoid tac (err, info) c =
 		[Proofview.V82.tactic (refine p);
 		 (* Might be ill-typed due to forbidden elimination. *)
 		 Tacticals.New.onLastHypId (tac (not isrec))]
-           end })))
+           end)))
           (Proofview.tclZERO ~info err)
     | None -> Proofview.tclZERO ~info err
   with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
-  end }
+  end
 
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
 
 let solve_remaining_apply_goals =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-  let sigma = Proofview.Goal.sigma gl in
+  Proofview.Goal.enter begin fun gl ->
+  let evd = Proofview.Goal.sigma gl in
   if !apply_solve_class_goals then
     try 
       let env = Proofview.Goal.env gl in
-      let evd = Sigma.to_evar_map sigma in
       let concl = Proofview.Goal.concl gl in
       if Typeclasses.is_class_type evd concl then
         let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in
-        let tac = Refine.refine ~unsafe:true { run = fun h -> Sigma.here c' h } in
-        Sigma.Unsafe.of_pair (tac, evd')
-	else Sigma.here (Proofview.tclUNIT ()) sigma
-    with Not_found -> Sigma.here (Proofview.tclUNIT ()) sigma
-  else Sigma.here (Proofview.tclUNIT ()) sigma
-  end }
+        Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd')
+        (Refine.refine ~unsafe:true (fun h -> (h,c')))
+	else Proofview.tclUNIT ()
+    with Not_found -> Proofview.tclUNIT ()
+  else Proofview.tclUNIT ()
+  end
 
 let tclORELSEOPT t k =
   Proofview.tclORELSE t
@@ -1695,7 +1681,7 @@ let tclORELSEOPT t k =
     | Some tac -> tac)
 
 let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : EConstr.constr with_bindings)) =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   let sigma = Tacmach.New.project gl in
   let flags =
@@ -1705,7 +1691,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
   step. *)
   let concl_nprod = nb_prod_modulo_zeta sigma concl in
   let rec try_main_apply with_destruct c =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
 
@@ -1759,14 +1745,14 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
       | PretypeError _|RefinerError _|UserError _|Failure _ ->
         Some (try_red_apply thm_ty0 (e, info))
       | _ -> None)
-    end }
+    end
   in
     Tacticals.New.tclTHENLIST [
       try_main_apply with_destruct c;
       solve_remaining_apply_goals;
       apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
     ]
-  end }
+  end
 
 let rec apply_with_bindings_gen b e = function
   | [] -> Proofview.tclUNIT ()
@@ -1778,13 +1764,13 @@ let rec apply_with_bindings_gen b e = function
 
 let apply_with_delayed_bindings_gen b e l = 
   let one k (loc, f) =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
-      let (cb, sigma) = run_delayed env sigma f in
+      let (sigma, cb) = f env sigma in
 	Tacticals.New.tclWITHHOLES e
           (general_apply b b e k (loc,cb)) sigma
-    end }
+    end
   in
   let rec aux = function
     | [] -> Proofview.tclUNIT ()
@@ -1861,7 +1847,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
 let apply_in_once sidecond_first with_delta with_destruct with_evars naming
     id (clear_flag,(loc,(d,lbind))) tac =
   let open Context.Rel.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let flags =
@@ -1870,7 +1856,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
   let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
   let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
   let rec aux idstoclear with_destruct c =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     try
@@ -1887,22 +1873,22 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
         (descend_in_conjunctions [targetid]
            (fun b id -> aux (id::idstoclear) b (mkVar id))
            (e, info) c)
-    end }
+    end
   in
   aux [] with_destruct d
-  end }
+  end
 
 let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
     id (clear_flag,(loc,f)) tac =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-    let (c, sigma) = run_delayed env sigma f in
+    let (sigma, c) = f env sigma in
     Tacticals.New.tclWITHHOLES with_evars 
       (apply_in_once sidecond_first with_delta with_destruct with_evars
          naming id (clear_flag,(loc,c)) tac)
       sigma
-  end }
+  end
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -1922,21 +1908,20 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
 *)
 
 let cut_and_apply c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
       | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
-        Refine.refine { run = begin fun sigma ->
+        Refine.refine begin fun sigma ->
           let typ = mkProd (Anonymous, c2, concl) in
-          let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in
-          let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in
-          let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
-          Sigma (ans, sigma, p +> q)
-        end }
+          let (sigma, f) = Evarutil.new_evar env sigma typ in
+          let (sigma, x) = Evarutil.new_evar env sigma c1 in
+          (sigma, mkApp (f, [|mkApp (c, [|x|])|]))
+        end
       | _ -> error "lapply needs a non-dependent product."
-  end }
+  end
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -1949,42 +1934,38 @@ let cut_and_apply c =
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
 let exact_no_check c =
-  Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
+  Refine.refine ~unsafe:true (fun h -> (h,c))
 
 let exact_check c =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   (** We do not need to normalize the goal because we just check convertibility *)
   let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
   let env = Proofview.Goal.env gl in
-  let sigma = Sigma.to_evar_map sigma in
   let sigma, ct = Typing.type_of env sigma c in
-  let tac =
-      Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c)
-  in
-  Sigma.Unsafe.of_pair (tac, sigma)
-  end }
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c))
+  end
 
 let cast_no_check cast c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     exact_no_check (mkCast (c, cast, concl))
-  end }
+  end
 
 let vm_cast_no_check c = cast_no_check Term.VMcast c
 let native_cast_no_check c = cast_no_check Term.NATIVEcast c
 
 let exact_proof c =
   let open Tacmach.New in
-  Proofview.Goal.enter { enter = begin fun gl ->
-  Refine.refine { run = begin fun sigma ->
-    let sigma = Sigma.to_evar_map sigma in
+  Proofview.Goal.enter begin fun gl ->
+  Refine.refine begin fun sigma ->
     let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
     let c = EConstr.of_constr c in
     let sigma = Evd.merge_universe_context sigma ctx in
-    Sigma.Unsafe.of_pair (c, sigma)
-  end }
-  end }
+    (sigma, c)
+  end
+  end
 
 let assumption =
   let rec arec gl only_eq = function
@@ -2008,10 +1989,10 @@ let assumption =
 	exact_no_check (mkVar (NamedDecl.get_id decl))
     else arec gl only_eq rest
   in
-  let assumption_tac = { enter = begin fun gl ->
+  let assumption_tac gl =
     let hyps = Proofview.Goal.hyps gl in
     arec gl true hyps
-  end } in
+  in
   Proofview.Goal.enter assumption_tac
 
 (*****************************************************************)
@@ -2050,7 +2031,7 @@ let check_decl env sigma decl =
 
 let clear_body ids =
   let open Context.Named.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
     let sigma = Tacmach.New.project gl in
@@ -2095,10 +2076,10 @@ let clear_body ids =
         Tacticals.New.tclZEROMSG msg
     in
     check <*>
-    Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
-    end }
-  end }
+    end
+  end
 
 let clear_wildcards ids =
   Tacticals.New.tclMAP (fun (loc, id) -> clear [id]) ids
@@ -2117,7 +2098,7 @@ let rec intros_clearing = function
 (* Keeping only a few hypotheses *)
 
 let keep hyps =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   Proofview.tclENV >>= fun env ->
   let ccl = Proofview.Goal.concl gl in
   let sigma = Tacmach.New.project gl in
@@ -2133,7 +2114,7 @@ let keep hyps =
       ~init:([],[]) (Proofview.Goal.env gl)
   in
   clear cl
-  end }
+  end
 
 (*********************************)
 (*  Basic generalization tactics *)
@@ -2144,16 +2125,16 @@ let keep hyps =
    this generalizes [hyps |- goal] into [hyps |- T] *)
 
 let apply_type newcl args =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
-    Refine.refine { run = begin fun sigma ->
-      let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in
-      let Sigma (ev, sigma, p) =
+    Refine.refine begin fun sigma ->
+      let newcl = nf_betaiota sigma newcl (* As in former Logic.refine *) in
+      let (sigma, ev) =
         Evarutil.new_evar env sigma ~principal:true ~store newcl in
-      Sigma (applist (ev, args), sigma, p)
-    end }
-  end }
+      (sigma, applist (ev, args))
+    end
+  end
 
 (* Given a context [hyps] with domain [x1..xn], possibly with let-ins,
    and well-typed in the current goal, [bring_hyps hyps] generalizes
@@ -2162,25 +2143,25 @@ let apply_type newcl args =
 let bring_hyps hyps =
   if List.is_empty hyps then Tacticals.New.tclIDTAC
   else
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
       let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
-      Refine.refine { run = begin fun sigma ->
-        let Sigma (ev, sigma, p) =
+      Refine.refine begin fun sigma ->
+        let (sigma, ev) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
-        Sigma (mkApp (ev, args), sigma, p)
-      end }
-    end }
+        (sigma, mkApp (ev, args))
+      end
+    end
 
 let revert hyps = 
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
     let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
       (bring_hyps ctx) <*> (clear hyps)
-  end }
+  end
 
 (************************)
 (* Introduction tactics *)
@@ -2197,7 +2178,7 @@ 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.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let cl = Tacmach.New.pf_concl gl in
     let reduce_to_quantified_ind =
@@ -2208,19 +2189,16 @@ let constructor_tac with_evars expctdnumopt i lbind =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
       check_number_of_constructors expctdnumopt i nconstr;
 
-      let Sigma ((cons, u), sigma, p) = Sigma.fresh_constructor_instance
+      let (sigma, (cons, u)) = Evd.fresh_constructor_instance
 	(Proofview.Goal.env gl) sigma (fst mind, i) in
       let cons = mkConstructU (cons, EInstance.make u) in
 	
       let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
-      let tac =
-	(Tacticals.New.tclTHENLIST
-           [
-	    convert_concl_no_check redcl DEFAULTcast;
-	    intros; apply_tac])
-      in
-      Sigma (tac, sigma, p)
-  end }
+      Tacticals.New.tclTHENLIST
+         [ Proofview.Unsafe.tclEVARS sigma;
+           convert_concl_no_check redcl DEFAULTcast;
+           intros; apply_tac]
+  end
 
 let one_constructor i lbind = constructor_tac false None i lbind
 
@@ -2237,7 +2215,7 @@ let rec tclANY tac = function
 let any_constructor with_evars tacopt =
   let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
   let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let cl = Tacmach.New.pf_concl gl in
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
@@ -2247,7 +2225,7 @@ let any_constructor with_evars tacopt =
       Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
     if Int.equal nconstr 0 then error "The type has no constructors.";
     tclANY tac (List.interval 1 nconstr)
- end }
+ 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
@@ -2298,7 +2276,7 @@ let my_find_eq_data_decompose gl t =
   | Constr_matching.PatternMatchingFailure -> None
 
 let intro_decomp_eq ?loc l thin tac id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -2309,10 +2287,10 @@ let intro_decomp_eq ?loc l thin tac id =
     (eq,t,eq_args) (c, t)
   | None ->
     Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
-  end }
+  end
 
 let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
   let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -2324,7 +2302,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
     (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
     (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
        nv_with_let ll)
-  end }
+  end
 
 let rewrite_hyp_then assert_style with_evars thin l2r id tac =
   let rew_on l2r =
@@ -2334,7 +2312,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
   let clear_var_and_eq id' = clear [id';id] in
   let early_clear id' thin =
     List.filter (fun (_,id) -> not (Id.equal id id')) thin in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
@@ -2366,7 +2344,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
         thin in
     (* Skip the side conditions of the rewriting step *)
     Tacticals.New.tclTHENFIRST eqtac (tac thin)
-  end }
+  end 
 
 let prepare_naming ?loc = function
   | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id)
@@ -2525,10 +2503,8 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
         else
           clear [id] in
-      let f = { delayed = fun env sigma ->
-        let Sigma (c, sigma, p) = f.delayed env sigma in
-        Sigma ((c, NoBindings), sigma, p)
-      } in
+      let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings))
+      in
       apply_in_delayed_once false true true with_evars naming id (None,(loc',f))
         (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
@@ -2547,12 +2523,12 @@ and prepare_intros ?loc with_evars dft destopt = function
       (str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_head_core with_evars b destopt bound pat =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     check_name_unicity env [] [] pat;
     intro_patterns_core with_evars b [] [] [] destopt
       bound 0 (fun _ l -> clear_wildcards l) pat
-  end }
+  end
 
 let intro_patterns_bound_to with_evars n destopt =
   intro_patterns_head_core with_evars true destopt
@@ -2602,7 +2578,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   let tac (naming,lemma) tac id =
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let destopt =
     if with_evars then MoveLast (* evars would depend on the whole context *)
     else get_previous_hyp_position id gl in
@@ -2614,7 +2590,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   in
   (* We chain apply_in_once, ending with an intro pattern *)
   List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
-  end }
+  end
 
 (*
   if sidecond_first then
@@ -2625,7 +2601,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
 *)
 
 let apply_in simple with_evars id lemmas ipat =
-  let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, { delayed = fun _ sigma -> Sigma.here l sigma })) lemmas in
+  let lemmas = List.map (fun (k,(loc,l)) -> k, (loc, (fun _ sigma -> (sigma,l)))) lemmas in
   general_apply_in false simple simple with_evars id lemmas ipat
 
 let apply_delayed_in simple with_evars id lemmas ipat =
@@ -2649,17 +2625,16 @@ let decode_hyp = function
 *)
 
 let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let Sigma (t, sigma, p) = match ty with
-    | Some t -> Sigma.here t sigma
+    let (sigma, t) = match ty with
+    | Some t -> (sigma, t)
     | None ->
       let t = typ_of env sigma c in
-      let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in
-      Sigma.Unsafe.of_pair (c, sigma)
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t
     in
-    let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with
+    let (sigma, (newcl, eq_tac)) = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
             | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl
@@ -2667,33 +2642,31 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
             | IntroIdentifier id -> id in
           let eqdata = build_coq_eq_data () in
           let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
-          let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in
+          let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
           let eq = EConstr.of_constr eq in
-          let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in
+          let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
           let refl = EConstr.of_constr refl in
           let eq = applist (eq,args) in
           let refl = applist (refl, [t;mkVar id]) in
 	  let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
-	  let sigma = Sigma.to_evar_map sigma in
 	  let sigma, _ = Typing.type_of env sigma term in
           let ans = term,
-            Tacticals.New.tclTHEN
-	      (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
-	      (clear_body [heq;id])
+            Tacticals.New.tclTHENLIST
+	      [
+               intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false;
+	      clear_body [heq;id]]
           in
-          Sigma.Unsafe.of_pair (ans, sigma)
+          (sigma, ans)
       | None ->
-          Sigma.here (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) sigma
+          (sigma, (mkNamedLetIn id c t ccl, Proofview.tclUNIT ()))
     in
-    let tac =
       Tacticals.New.tclTHENLIST
-      [ convert_concl_no_check newcl DEFAULTcast;
+      [ Proofview.Unsafe.tclEVARS sigma;
+        convert_concl_no_check newcl DEFAULTcast;
         intro_gen (NamingMustBe (Loc.tag id)) (decode_hyp lastlhyp) true false;
         Tacticals.New.tclMAP convert_hyp_no_check depdecls;
         eq_tac ]
-    in
-    Sigma (tac, sigma, p +> q)
-  end }
+  end
 
 let insert_before decls lasthyp env =
   match lasthyp with
@@ -2725,22 +2698,22 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
           id in
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
-      let Sigma (eq, sigma, p) = Sigma.fresh_global env sigma eqdata.eq in
+      let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
       let eq = EConstr.of_constr eq in
-      let Sigma (refl, sigma, q) = Sigma.fresh_global env sigma eqdata.refl in
+      let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
       let refl = EConstr.of_constr refl in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
-      let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in
-      Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r)
+      let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+      (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
   | None ->
       let newenv = insert_before [decl] lastlhyp env in
-      let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in
-      Sigma (mkNamedLetIn id c t x, sigma, p)
+      let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+      (sigma, mkNamedLetIn id c t x)
 
 let letin_tac with_eq id c ty occs =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
@@ -2748,41 +2721,39 @@ let letin_tac with_eq id c ty occs =
     let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
     (* We keep the original term to match but record the potential side-effects
        of unifying universes. *)
-    let Sigma (c, sigma, p) = match res with
-      | None -> Sigma.here c sigma
-      | Some (Sigma (_, sigma, p)) -> Sigma (c, sigma, p)
+    let (sigma, c) = match res with
+      | None -> (sigma, c)
+      | Some (sigma, _) -> (sigma, c)
     in
-    let tac = letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty in
-    Sigma (tac, sigma, p)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty)
+  end
 
 let letin_pat_tac with_evars with_eq id c occs =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let ccl = Proofview.Goal.concl gl in
     let check t = true in
     let abs = AbstractPattern (false,check,id,c,occs,false) in
     let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
-    let Sigma (c, sigma, p) = match res with
+    let (sigma, c) = match res with
     | None -> finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma c
     | Some res -> res in
-    let tac =
-      (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None)
-    in
-    Sigma (tac, sigma, p)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None)
+  end
 
 (* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *)
 let forward b usetac ipat c =
   match usetac with
   | None ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
       let t = Tacmach.New.pf_get_type_of gl c in
       let sigma = Tacmach.New.project gl in
       let hd = head_ident sigma c in
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
-      end }
+      end
   | Some tac ->
       let tac = match tac with
         | None -> Tacticals.New.tclIDTAC
@@ -2847,7 +2818,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
 let generalize_dep ?(with_let=false) c =
   let open Tacmach.New in
   let open Tacticals.New in
-  Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let env = pf_env gl in
   let sign = Proofview.Goal.hyps gl in
   let sigma = project gl in
@@ -2881,16 +2852,14 @@ let generalize_dep ?(with_let=false) c =
   (** Check that the generalization is indeed well-typed *)
   let (evd, _) = Typing.type_of env evd cl'' in
   let args = Context.Named.to_instance mkVar to_quantify_rev in
-  let tac =
-    tclTHEN
-      (apply_type cl'' (if Option.is_empty body then c::args else args))
-      (clear (List.rev tothin'))
-  in
-  Sigma.Unsafe.of_pair (tac, evd)
-  end }
+  tclTHENLIST
+    [ Proofview.Unsafe.tclEVARS evd;
+      apply_type cl'' (if Option.is_empty body then c::args else args);
+      clear (List.rev tothin')]
+  end
 
 (**  *)
-let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
+let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let newcl, evd =
     List.fold_right_i (generalize_goal gl) 0 lconstr
@@ -2898,16 +2867,15 @@ let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl
   in
   let (evd, _) = Typing.type_of env evd newcl in
   let map ((_, c, b),_) = if Option.is_empty b then Some c else None in
-  let tac = apply_type newcl (List.map_filter map lconstr) in
-  Sigma.Unsafe.of_pair (tac, evd)
-end }
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd)
+  (apply_type newcl (List.map_filter map lconstr))
+end
 
 let new_generalize_gen_let lconstr =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
-    let sigma = Sigma.to_evar_map sigma in
     let env = Proofview.Goal.env gl in
     let ids = Tacmach.New.pf_ids_of_hyps gl in
     let newcl, sigma, args =
@@ -2919,14 +2887,12 @@ let new_generalize_gen_let lconstr =
           (cl, sigma, args))
 	0 lconstr (concl, sigma, [])
     in
-    let tac =
-	Refine.refine { run = begin fun sigma ->
-          let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in
-          Sigma ((applist (ev, args)), sigma, p)
-	end }
-    in
-    Sigma.Unsafe.of_pair (tac, sigma)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+	(Refine.refine begin fun sigma ->
+          let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true newcl in
+          (sigma, applist (ev, args))
+	 end)
+  end
 
 let generalize_gen lconstr =
   generalize_gen_let (List.map (fun (occs_c,na) ->
@@ -2968,9 +2934,9 @@ let quantify lconstr =
    of inferred args and yi. The overall effect is to remove from H as
    much quantification as possible given lbind. *)
 let specialize (c,lbind) ipat =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+  let sigma = Proofview.Goal.sigma gl in
   let sigma, term =
     if lbind == NoBindings then
       sigma, c
@@ -3046,7 +3012,7 @@ let specialize (c,lbind) ipat =
 	  (exact_no_check term)
   in
   Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
-  end }
+  end
 
 (*****************************)
 (* Ad hoc unfold             *)
@@ -3056,7 +3022,7 @@ let specialize (c,lbind) ipat =
 (* Unfolds x by its definition everywhere *)
 let unfold_body x =
   let open Context.Named.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
   let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
   let xval = match Environ.lookup_named x env with
@@ -3072,7 +3038,7 @@ let unfold_body x =
   let reductc = reduct_in_concl (rfun, DEFAULTcast) in
   Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
   end
-  end }
+  end
 
 (* Either unfold and clear if defined or simply clear if not a definition *)
 let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
@@ -3117,7 +3083,7 @@ let warn_unused_intro_pattern =
           strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
           ++ str": " ++ prlist_with_sep spc 
          (Miscprint.pr_intro_pattern 
-	 (fun c -> Printer.pr_econstr (fst (run_delayed (Global.env()) Evd.empty c)))) names)
+	 (fun c -> Printer.pr_econstr (snd (c (Global.env()) Evd.empty)))) names)
 
 let check_unused_names names =
   if not (List.is_empty names) then
@@ -3201,7 +3167,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
     match ra with
     | (RecArg,_,deprec,recvarname) ::
         (IndArg,_,depind,hyprecname) :: ra' ->
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
         let (recpat,names) = match names with
           | [loc,IntroNaming (IntroIdentifier id) as pat] ->
               let id' = next_ident_away (add_prefix "IH" id) avoid in
@@ -3209,37 +3175,37 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
           | _ -> consume_pattern avoid (Name recvarname) deprec gl names in
         let dest = get_recarg_dest dests in
         dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin ->
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
           let (hyprec,names) =
             consume_pattern avoid (Name hyprecname) depind gl names
           in
 	  dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin ->
 	    peel_tac ra' (update_dest dests ids') names thin)
-        end })
-        end }
+                             end)
+        end
     | (IndArg,_,dep,hyprecname) :: ra' ->
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names =
           consume_pattern avoid (Name hyprecname) dep gl names in
 	dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
-        end }
+        end
     | (RecArg,_,dep,recvarname) :: ra' ->
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
         let (pat,names) =
           consume_pattern avoid (Name recvarname) dep gl names in
         let dest = get_recarg_dest dests in
 	dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
-        end }
+        end
     | (OtherArg,_,dep,_) :: ra' ->
-        Proofview.Goal.enter { enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
         let (pat,names) = consume_pattern avoid Anonymous dep gl names in
         let dest = get_recarg_dest dests in
 	safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
-        end }
+        end
     | [] ->
         check_unused_names names;
         Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests)
@@ -3262,7 +3228,7 @@ let expand_projections env sigma c =
 (* Marche pas... faut prendre en compte l'occurrence précise... *)
 
 let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in
@@ -3316,7 +3282,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
 	      (atomize_one (i-1) (mkVar x::args) (mkVar x::args') (x::avoid))
   in
   atomize_one (List.length argl) [] [] []
-  end }
+  end
 
 (* [cook_sign] builds the lists [beforetoclear] (preceding the
    ind. var.) and [aftertoclear] (coming after the ind. var.)  of hyps
@@ -3561,16 +3527,12 @@ let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
   user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
-let glob sigma gr =
-  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
-  in Sigma.to_evar_map sigma, c
-
-let coq_eq sigma       = glob sigma (Coqlib.build_coq_eq ())
-let coq_eq_refl sigma  = glob sigma (Coqlib.build_coq_eq_refl ())
+let coq_eq sigma       = Evarutil.new_global sigma (Coqlib.build_coq_eq ())
+let coq_eq_refl sigma  = Evarutil.new_global sigma (Coqlib.build_coq_eq_refl ())
 
 let coq_heq_ref        = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq")
-let coq_heq sigma      = glob sigma (Lazy.force coq_heq_ref)
-let coq_heq_refl sigma = glob sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
+let coq_heq sigma      = Evarutil.new_global sigma (Lazy.force coq_heq_ref)
+let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
 
 let mkEq sigma t x y =
   let sigma, eq = coq_eq sigma in
@@ -3625,25 +3587,24 @@ let decompose_indapp sigma f args =
   | _ -> f, args
 
 let mk_term_eq homogeneous env sigma ty t ty' t' =
-  let sigma = Sigma.to_evar_map sigma in
   if homogeneous then
     let sigma, eq = mkEq sigma ty t t' in
     let sigma, refl = mkRefl sigma ty' t' in
-    Sigma.Unsafe.of_evar_map sigma, (eq, refl)
+    sigma, (eq, refl)
   else
     let sigma, heq = mkHEq sigma ty t ty' t' in
     let sigma, hrefl = mkHRefl sigma ty' t' in
-    Sigma.Unsafe.of_evar_map sigma, (heq, hrefl)
+    sigma, (heq, hrefl)
 
 let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   let open Context.Rel.Declaration in
-  Refine.refine { run = begin fun sigma ->
+  Refine.refine begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
   let sigma, abshypeq, abshypt =
     if dep then
       let ty = lift 1 c in
-      let homogeneous = Reductionops.is_conv env (Sigma.to_evar_map sigma) ty typ in
+      let homogeneous = Reductionops.is_conv env sigma ty typ in
       let sigma, (eq, refl) =
         mk_term_eq homogeneous (push_rel_context ctx env) sigma ty (mkRel 1) typ (mkVar id) in
       sigma, mkProd (Anonymous, eq, lift 1 concl), [| refl |]
@@ -3661,7 +3622,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
     (* Abstract by the extension of the context *)
   let genctyp = it_mkProd_or_LetIn genarg ctx in
     (* The goal will become this product. *)
-  let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in
+  let (sigma, genc) = Evarutil.new_evar env sigma ~principal:true genctyp in
     (* Apply the old arguments giving the proper instantiation of the hyp *)
   let instc = mkApp (genc, Array.of_list args) in
     (* Then apply to the original instantiated hyp. *)
@@ -3669,8 +3630,8 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
     (* Apply the reflexivity proofs on the indices. *)
   let appeqs = mkApp (instc, Array.of_list refls) in
     (* Finally, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
-  Sigma (mkApp (appeqs, abshypt), sigma, p)
-  end }
+  (sigma, mkApp (appeqs, abshypt))
+  end
 
 let hyps_of_vars env sigma sign nogen hyps =
   if Id.Set.is_empty hyps then []
@@ -3802,7 +3763,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 
 let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
   let open Context.Named.Declaration in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   Coqlib.check_required_library Coqlib.jmeq_module_name;
   let sigma = Tacmach.New.project gl in
   let (f, args, def, id, oldid) =
@@ -3838,7 +3799,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
                 [revert vars ;
 		 Tacticals.New.tclMAP (fun id ->
 		      Tacticals.New.tclTRY (generalize_dep ~with_let:true (mkVar id))) vars])
-  end }
+  end
 
 let compare_upto_variables sigma x y =
   let rec compare x y =
@@ -3899,12 +3860,12 @@ let specialize_eqs id gl =
     else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
 
 
-let specialize_eqs id = Proofview.Goal.enter { enter = begin fun gl ->
+let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
   let msg = str "Specialization not allowed on dependent hypotheses" in
   Proofview.tclOR (clear [id])
     (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
     Proofview.V82.tactic (specialize_eqs id)
-end }
+end
 
 let occur_rel sigma n c =
   let res = not (noccurn sigma n c) in
@@ -4118,17 +4079,17 @@ let guess_elim isrec dep s hyp0 gl =
     if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
     else
       let env = Tacmach.New.pf_env gl in
-      let sigma = Sigma.Unsafe.of_evar_map (Tacmach.New.project gl) in
+      let sigma = Tacmach.New.project gl in
       let u = EInstance.kind (Tacmach.New.project gl) u in
       if use_dependent_propositions_elimination () && dep
       then
-        let Sigma (ind, sigma, _) = build_case_analysis_scheme env sigma (mind, u) true s in
+        let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
-        (Sigma.to_evar_map sigma, ind)
+        (sigma, ind)
       else
-        let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma (mind, u) s in
+        let (sigma, ind) = build_case_analysis_scheme_default env sigma (mind, u) s in
         let ind = EConstr.of_constr ind in
-        (Sigma.to_evar_map sigma, ind)
+        (sigma, ind)
   in
   let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
     evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
@@ -4235,7 +4196,7 @@ let recolle_clenv i params args elimclause gl =
     produce new ones). Then refine with the resulting term with holes.
 *)
 let induction_tac with_evars params indvars elim =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Tacmach.New.project gl in
   let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
   let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in
@@ -4248,17 +4209,16 @@ let induction_tac with_evars params indvars elim =
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
   enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
-  end }
+  end
 
 (* Apply induction "in place" taking into account dependent
    hypotheses from the context, replacing the main hypothesis on which
    induction applies with the induction hypotheses *)
 
 let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let sigma = Sigma.to_evar_map sigma in
     let concl = Tacmach.New.pf_concl gl in
     let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in
     let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in
@@ -4288,16 +4248,16 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
             (re_intro_dependent_hypotheses statuslists))
          indsign names)
     in
-    Sigma.Unsafe.of_pair (tac, sigma)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
+  end
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in
   atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
     apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
       (fun elim -> induction_tac with_evars [] [hyp0] elim))
-  end }
+  end
 
 let msg_not_right_number_induction_arguments scheme =
   str"Not the right number of induction arguments (expected " ++
@@ -4314,7 +4274,7 @@ let msg_not_right_number_induction_arguments scheme =
    must be given, so we help a bit the unifier by making the "pattern"
    by hand before calling induction_tac *)
 let induction_without_atomization isrec with_evars elim names lid =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in
   let nargs_indarg_farg =
     scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in
@@ -4345,11 +4305,11 @@ let induction_without_atomization isrec with_evars elim names lid =
   ] in
   let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
   apply_induction_in_context with_evars None [] elim indvars names induct_tac
-  end }
+  end
 
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
   then user_err 
@@ -4367,10 +4327,9 @@ let clear_unselected_context id inhyps cls =
       let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in
       clear ids
   | None -> Proofview.tclUNIT ()
-  end }
+  end
 
 let use_bindings env sigma elim must_be_closed (c,lbind) typ =
-  let sigma = Sigma.to_evar_map sigma in
   let typ =
     if elim == None then
       (* w/o an scheme, the term has to be applied at least until
@@ -4392,8 +4351,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
       if must_be_closed && occur_meta indclause.evd (clenv_value indclause) then
         error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
-      let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
-      Sigma.Unsafe.of_pair (c, sigma)
+      pose_all_metas_as_evars env indclause.evd (clenv_value indclause)
     with e when catchable_exception e ->
     try find_clause (try_red_product env sigma typ)
     with Redelimination -> raise e in
@@ -4411,7 +4369,6 @@ let check_expected_type env sigma (elimc,bl) elimt =
   fun t -> Evarconv.e_cumul env (ref sigma) t u
 
 let check_enough_applied env sigma elim =
-  let sigma = Sigma.to_evar_map sigma in
   (* A heuristic to decide whether the induction arg is enough applied *)
   match elim with
   | None ->
@@ -4436,13 +4393,13 @@ let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
 
 let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
      id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let ccl = Proofview.Goal.concl gl in
   let store = Proofview.Goal.extra gl in
   let check = check_enough_applied env sigma elim in
-  let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in
+  let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in
   let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
   let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in
   match res with
@@ -4452,7 +4409,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       (* we restart using bindings after having tried type-class
          resolution etc. on the term given by the user *)
       let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in
-      let Sigma (c0, sigma, q) = finish_evar_resolution ~flags env sigma (pending,c0) in
+      let (sigma, c0) = finish_evar_resolution ~flags env sigma (pending,c0) in
       let tac =
       (if isrec then
           (* Historically, induction has side conditions last *)
@@ -4461,13 +4418,12 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           (* and destruct has side conditions first *)
           Tacticals.New.tclTHENLAST)
       (Tacticals.New.tclTHENLIST [
-        Refine.refine ~unsafe:true { run = begin fun sigma ->
+        Refine.refine ~unsafe:true begin fun sigma ->
           let b = not with_evars && with_eq != None in
-          let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in
-          let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
-          let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in
-          Sigma (ans, sigma, p +> q)
-        end };
+          let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in
+          let t = Retyping.get_type_of env sigma c in
+          mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+        end;
         if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
         if is_arg_pure_hyp
         then Proofview.tclEVARMAP >>= fun sigma -> Tacticals.New.tclTRY (clear [destVar sigma c0])
@@ -4476,23 +4432,23 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       ])
       tac
       in
-      Sigma (tac, sigma, q)
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
 
-  | Some (Sigma (c, sigma', q)) ->
+  | Some (sigma', c) ->
       (* pattern found *)
       let with_eq = Option.map (fun eq -> (false,eq)) eqname in
       (* TODO: if ind has predicate parameters, use JMeq instead of eq *)
       let env = reset_with_named_context sign env in
       let tac =
       Tacticals.New.tclTHENLIST [
-        Refine.refine ~unsafe:true { run = begin fun sigma ->
+        Refine.refine ~unsafe:true begin fun sigma ->
           mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
-        end };
+        end;
         tac
       ]
       in
-      Sigma (tac, sigma', p +> q)
-  end }
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma') tac
+  end
 
 let has_generic_occurrences_but_goal cls id env sigma ccl =
   clause_with_generic_context_selection cls &&
@@ -4504,19 +4460,18 @@ let induction_gen clear_flag isrec with_evars elim
   let inhyps = match cls with
   | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
   | _ -> [] in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
-  let evd = Sigma.to_evar_map sigma in
+  let evd = Proofview.Goal.sigma gl in
   let ccl = Proofview.Goal.concl gl in
   let cls = Option.default allHypsAndConcl cls in
-  let t = typ_of env sigma c in
+  let t = typ_of env evd c in
   let is_arg_pure_hyp =
     isVar evd c && not (mem_named_context_val (destVar evd c) (Global.named_context_val ()))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && clear_flag == None
     && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in
-  let enough_applied = check_enough_applied env sigma elim t in
+  let enough_applied = check_enough_applied env evd elim t in
   if is_arg_pure_hyp && enough_applied then
     (* First case: induction on a variable already in an inductive type and
        with maximal abstraction over the variable.
@@ -4540,7 +4495,7 @@ let induction_gen clear_flag isrec with_evars elim
       isrec with_evars info_arg elim id arg t inhyps cls
     (induction_with_atomization_of_ind_arg
        isrec with_evars elim names id inhyps)
-  end }
+  end 
 
 (* Induction on a list of arguments. First make induction arguments
    atomic (using letins), then do induction. The specificity here is
@@ -4566,7 +4521,7 @@ let induction_gen_l isrec with_evars elim names lc =
 		atomize_list l'
 
 	    | _ ->
-                Proofview.Goal.enter { enter = begin fun gl ->
+                Proofview.Goal.enter begin fun gl ->
                 let type_of = Tacmach.New.pf_unsafe_type_of gl in
                 let sigma = Tacmach.New.project gl in
                 let x =
@@ -4578,7 +4533,7 @@ let induction_gen_l isrec with_evars elim names lc =
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
 		  (atomize_list newl')
-                end } in
+                end in
   Tacticals.New.tclTHENLIST
     [
       (atomize_list lc);
@@ -4595,7 +4550,7 @@ let induction_destruct isrec with_evars (lc,elim) =
   match lc with
   | [] -> assert false (* ensured by syntax, but if called inside caml? *)
   | [c,(eqname,names as allnames),cls] ->
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     match elim with
@@ -4612,9 +4567,9 @@ let induction_destruct isrec with_evars (lc,elim) =
       (* standard induction *)
       onOpenInductionArg env sigma
       (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c
-    end }
+    end
   | _ ->
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     match elim with
@@ -4630,12 +4585,12 @@ let induction_destruct isrec with_evars (lc,elim) =
         (onOpenInductionArg env sigma (fun clear_flag a ->
           induction_gen clear_flag isrec with_evars None (a,b) cl) a)
         (Tacticals.New.tclMAP (fun (a,b,cl) ->
-          Proofview.Goal.enter { enter = begin fun gl ->
+          Proofview.Goal.enter begin fun gl ->
           let env = Proofview.Goal.env gl in
           let sigma = Tacmach.New.project gl in      
           onOpenInductionArg env sigma (fun clear_flag a ->
             induction_gen clear_flag false with_evars None (a,b) cl) a
-          end }) l)
+          end) l)
     | Some elim ->
       (* Several induction hyps with induction scheme *)
       let lc = List.map (on_pi1 (fun c -> snd (force_destruction_arg false env sigma c))) lc in
@@ -4654,7 +4609,7 @@ let induction_destruct isrec with_evars (lc,elim) =
         error "'as' clause with multiple arguments and 'using' clause can only occur last.";
       let newlc = List.map (fun (x,_) -> (x,None)) newlc in
       induction_gen_l isrec with_evars elim names newlc
-    end }
+    end
 
 let induction ev clr c l e =
   induction_gen clr true ev e 
@@ -4696,7 +4651,7 @@ let simple_destruct = function
  *)
 
 let elim_scheme_type elim t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let clause = mk_clenv_type_of gl elim in
   match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
     | Meta mv ->
@@ -4706,26 +4661,26 @@ let elim_scheme_type elim t =
             (clenv_meta_type clause mv) clause in
 	Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
     | _ -> anomaly (Pp.str "elim_scheme_type.")
-  end }
+  end
 
 let elim_type t =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
   let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
-  Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd)
-  end }
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t)
+  end
 
 let case_type t =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let env = Tacmach.New.pf_env gl in
-  let ((ind, u), t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in
-  let u = EInstance.kind (Sigma.to_evar_map sigma) u in
+  let ((ind, u), t) = reduce_to_atomic_ind env sigma t in
+  let u = EInstance.kind sigma u in
   let s = Tacticals.New.elimination_sort_of_goal gl in
-  let Sigma (elimc, evd, p) = build_case_analysis_scheme_default env sigma (ind, u) s in
+  let (evd, elimc) = build_case_analysis_scheme_default env sigma (ind, u) s in
   let elimc = EConstr.of_constr elimc in
-  Sigma (elim_scheme_type elimc t, evd, p)
-  end }
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) (elim_scheme_type elimc t)
+  end
 
 
 (************************************************)
@@ -4745,7 +4700,7 @@ let maybe_betadeltaiota_concl allowred gl =
     whd_all env sigma concl
 
 let reflexivity_red allowred =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   (* PL: usual reflexivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -4754,7 +4709,7 @@ let reflexivity_red allowred =
     match match_with_equality_type sigma concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
-  end }
+  end
 
 let reflexivity =
   Proofview.tclORELSE
@@ -4796,7 +4751,7 @@ let match_with_equation sigma c =
     Proofview.tclZERO NoEquationFound
 
 let symmetry_red allowred =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   (* PL: usual symmetry don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -4809,7 +4764,7 @@ let symmetry_red allowred =
         (convert_concl_no_check concl DEFAULTcast)
         (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
-  end }
+  end
 
 let symmetry =
   Proofview.tclORELSE
@@ -4823,7 +4778,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 
 let symmetry_in id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Tacmach.New.project gl in
   let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
   let sign,t = decompose_prod_assum sigma ctype in
@@ -4843,7 +4798,7 @@ let symmetry_in id =
       | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
       | e -> Proofview.tclZERO ~info e
     end
-  end }
+  end
 
 let intros_symmetry =
   Tacticals.New.onClause
@@ -4868,7 +4823,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_transitivity hdcncl eq_kind t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let (eq1,eq2) = match eq_kind with
   | MonomorphicLeibnizEq (c1,c2) ->
       mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
@@ -4888,10 +4843,10 @@ let prove_transitivity hdcncl eq_kind t =
 	  [ Tacticals.New.tclDO 2 intro;
 	    Tacticals.New.onLastHyp simplest_case;
 	    assumption ]))
-  end }
+  end
 
 let transitivity_red allowred t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   (* PL: usual transitivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -4909,7 +4864,7 @@ let transitivity_red allowred t =
       match t with
       | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
       | Some t -> prove_transitivity eq eq_kind t
-  end }
+  end
 
 let transitivity_gen t =
   Proofview.tclORELSE
@@ -4994,11 +4949,10 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
   let open Proofview.Notations in
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let current_sign = Global.named_context_val ()
   and global_sign = Proofview.Goal.hyps gl in
-  let sigma = Sigma.to_evar_map sigma in
   let evdref = ref sigma in
   let sign,secsign =
     List.fold_right
@@ -5065,8 +5019,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
     tacK lem args
   in
   let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in
-  Sigma.Unsafe.of_pair (tac, evd)
-  end }
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac
+  end
 
 let abstract_subproof ~opaque id gk tac =
   cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args)))
@@ -5093,7 +5047,7 @@ let tclABSTRACT ?(opaque=true) name_op tac =
   abstract_subproof ~opaque s gk tac
 
 let unify ?(state=full_transparent_state) x y =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   try
     let core_flags =
@@ -5106,12 +5060,11 @@ let unify ?(state=full_transparent_state) x y =
       merge_unify_flags = core_flags;
       subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } }
     in
-    let sigma = Sigma.to_evar_map sigma in
     let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
-    Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma)
+    Proofview.Unsafe.tclEVARS sigma
   with e when CErrors.noncritical e ->
-    Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma
-  end }
+    Tacticals.New.tclFAIL 0 (str"Not unifiable")
+  end
 
 module Simple = struct
   (** Simplified version of some of the above tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0dbcce02c5..ec8fe11456 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -29,7 +29,7 @@ open Locus
 
 (** {6 General functions. } *)
 
-val is_quantified_hypothesis : Id.t -> ('a, 'r) Proofview.Goal.t -> bool
+val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool
 
 (** {6 Primitive tactics. } *)
 
@@ -75,7 +75,7 @@ val intros               : unit Proofview.tactic
 (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
    the conclusion of goal [g], up to head-reduction if [b] is [true] *)
 val depth_of_quantified_hypothesis :
-  bool -> quantified_hypothesis -> ('a, 'r) Proofview.Goal.t -> int
+  bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int
 
 val intros_until         : quantified_hypothesis -> unit Proofview.tactic
 
@@ -131,7 +131,7 @@ val exact_proof      : Constrexpr.constr_expr -> unit Proofview.tactic
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-type change_arg = patvar_map -> constr Sigma.run
+type change_arg = patvar_map -> evar_map -> evar_map * constr
 
 val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
@@ -211,8 +211,6 @@ val apply_delayed_in :
     (clear_flag * delayed_open_constr_with_bindings located) list ->
     intro_pattern option -> unit Proofview.tactic
 
-val run_delayed : Environ.env -> evar_map -> 'a delayed_open -> 'a * evar_map
-
 (** {6 Elimination tactics. } *)
 
 (*
@@ -437,7 +435,7 @@ end
 
 module New : sig
 
-  val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic
+  val refine : ?unsafe:bool -> (evar_map -> evar_map * constr) -> unit Proofview.tactic
   (** [refine ?unsafe c] is [Refine.refine ?unsafe c]
       followed by beta-iota-reduction of the conclusion. *)