Remove the Sigma (monotonous state) API.

Reminder of (some of) the reasons for removal:

- Despite the claim in sigma.mli, it does *not* prevent evar
  leaks, something like:

  fun env evd ->
  let (evd',ev) = new_evar env evd in
  (evd,ev)

  will typecheck even with Sigma-like type annotations (with a proof of
  reflexivity)

- The API stayed embryonic. Even typing functions were not ported to
  Sigma.

- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
  less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
  at all (despite still being so).

- There was no good story for higher order functions manipulating evar
  maps. Without higher order, one can most of the time get away with
  reusing the same name for the updated evar map.

- Most of the code doing complex things with evar maps was using unsafe
  casts to sigma. This code should be fixed, but this is an orthogonal
  issue.

Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.

19 files changed, 713 insertions, 799 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e21396548..272cb1eda 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 9ed9f0ae2..a6fb82bab 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 de544fe5f..2d4f20276 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 672f9cffb..de49a521f 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 5e7090ded..83c2be410 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 986f53139..bae334461 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 855cb206f..13d64b8e3 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 93073fdc7..466b1350d 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 48ce52f09..0cee4b6ed 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 507ff10ee..efcefcf16 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 d64cc38ef..05c5cd5ec 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 70e62eaba..773abb9f0 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 9110830aa..a1d986544 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 b951e7ceb..ec038f638 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 83f3da30a..87d815fc8 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 a7eadc3c3..aa574e41c 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 96270f748..9603212de 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 a93a86d3a..b553f316c 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 0dbcce02c..ec8fe1145 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. *)