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.

11 files changed, 232 insertions, 288 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 0a13a20a9..ea1660d90 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -16,8 +16,6 @@ open Genredexpr
 open Stdarg
 open Extraargs
 
-open Sigma.Notations
-
 DECLARE PLUGIN "coretactics"
 
 (** Basic tactics *)
@@ -160,12 +158,12 @@ END
 (** Split *)
 
 let rec delayed_list = function
-| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma }
+| [] -> fun _ sigma -> (sigma, [])
 | x :: l ->
-  { Tacexpr.delayed = fun env sigma ->
-    let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in
-    let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in
-    Sigma (x :: l, sigma, p +> q) }
+  fun env sigma ->
+    let (sigma, x) = x env sigma in
+    let (sigma, l) = delayed_list l env sigma in
+    (sigma, x :: l)
 
 TACTIC EXTEND split
   [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ]
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index bf84f61a5..7db484d82 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -16,8 +16,6 @@ open Tacexpr
 open Refiner
 open Evd
 open Locus
-open Sigma.Notations
-open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -81,7 +79,7 @@ let instantiate_tac_by_name id c =
 
 let let_evar name typ =
   let src = (Loc.tag Evar_kinds.GoalEvar) in
-  Proofview.Goal.s_enter { s_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 sigma = ref sigma in
@@ -93,17 +91,14 @@ let let_evar name typ =
       Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
     | Names.Name id -> id
     in
-    let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
-    let tac =
-      (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
-    in
-    Sigma (tac, sigma, p)
-  end }
+    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+    (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
+  end
 
 let hget_evar n =
   let open EConstr in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
   let evl = evar_list sigma concl in
@@ -113,5 +108,5 @@ let hget_evar n =
   let ev = List.nth evl (n-1) in
   let ev_type = EConstr.existential_type sigma ev in
   Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
-  end }
+  end
 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 9726a5b40..8afe3053d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -24,7 +24,6 @@ open Util
 open Termops
 open Equality
 open Misctypes
-open Sigma.Notations
 open Proofview.Notations
 
 DECLARE PLUGIN "extratactics"
@@ -80,12 +79,12 @@ let induction_arg_of_quantified_hyp = function
    ElimOnIdent and not as "constr" *)
 
 let mytclWithHoles tac with_evars c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
     let sigma = Tacmach.New.project gl in
     let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in
     Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma'
-  end }
+  end
 
 let elimOnConstrWithHoles tac with_evars c =
   Tacticals.New.tclDELAYEDWITHHOLES with_evars c
@@ -115,7 +114,7 @@ END
 
 let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  discr_main { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
+  discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
 
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None) with_evars c
@@ -147,7 +146,7 @@ END
 
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
+  injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -354,23 +353,22 @@ let constr_flags () = {
   Pretyping.expand_evars = true }
 
 let refine_tac ist simple with_classes c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags =
       { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
-    let update = { run = fun sigma ->
-      let Sigma (c, sigma, p) = c.delayed env sigma in
-      Sigma (c, sigma, p)
-    } in
+    let update = begin fun sigma ->
+      c env sigma
+    end in
     let refine = Refine.refine ~unsafe:true update in
     if simple then refine
     else refine <*>
            Tactics.New.reduce_after_refine <*>
            Proofview.shelve_unifiable
-  end }
+  end
 
 TACTIC EXTEND refine
 | [ "refine" uconstr(c) ] ->
@@ -663,9 +661,8 @@ let subst_hole_with_term occ tc t =
 open Tacmach
 
 let hResolve id c occ t =
-  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 = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
   let env_ids = Termops.ids_of_context env in
@@ -684,11 +681,9 @@ let hResolve id c occ t =
   let t_constr = EConstr.of_constr t_constr in
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
-  let tac =
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))
-  in
-  Sigma.Unsafe.of_pair (tac, sigma)
-  end }
+  end
 
 let hResolve_auto id c t =
   let rec resolve_auto n = 
@@ -726,12 +721,12 @@ END
 exception Found of unit Proofview.tactic
 
 let rewrite_except h =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
   Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else 
       Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
     hyps
-  end }
+  end
 
 
 let refl_equal = 
@@ -745,29 +740,29 @@ let refl_equal =
   should be replaced by a call to the tactic but I don't know how to
   call it before it is defined. *)
 let  mkCaseEq a  : unit Proofview.tactic =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
     Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req ->
     Tacticals.New.tclTHENLIST
          [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))];
-          Proofview.Goal.enter { enter = begin fun gl ->
+          Proofview.Goal.enter begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
-            let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in
+            let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in
 	    change_concl c
-          end };
+          end;
 	  simplest_case a]
-  end }
+  end
 
 
 let case_eq_intros_rewrite x =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let hyps = Tacmach.New.pf_ids_of_hyps gl in
       let n' = nb_prod (Tacmach.New.project gl) concl in
@@ -776,9 +771,9 @@ let case_eq_intros_rewrite x =
                     Tacticals.New.tclDO (n'-n-1) intro;
 		    introduction h;
 		    rewrite_except h]
-    end }
+    end
   ]
-  end }
+  end
 
 let rec find_a_destructable_match sigma t =
   let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in
@@ -802,15 +797,15 @@ let destauto t =
   with Found tac -> tac
 
 let destauto_in id = 
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
 (*  Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
 (*  Pp.msgnl (Printer.pr_lconstr (ctype)); *)
   destauto ctype
-  end }
+  end
 
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
+| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ]
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
@@ -822,21 +817,21 @@ END
 (**********************************************************************)
 
 TACTIC EXTEND transparent_abstract
-| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
-      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
-| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
-      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+      Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+      Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ]
 END
 
 (* ********************************************************************* *)
 
 let eq_constr x y = 
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let evd = Tacmach.New.project gl in
       match EConstr.eq_constr_universes evd x y with
       | Some _ -> Proofview.tclUNIT () 
       | None -> Tacticals.New.tclFAIL 0 (str "Not equal")
-  end }
+  end
 
 TACTIC EXTEND constr_eq
 | [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ]
@@ -1082,7 +1077,7 @@ TACTIC EXTEND guard
 END
 
 let decompose l c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let to_ind c =
       if isInd sigma c then fst (destInd sigma c)
@@ -1090,7 +1085,7 @@ let decompose l c =
     in
     let l = List.map to_ind l in
     Elim.h_decompose l c
-  end }
+  end
 
 TACTIC EXTEND decompose
 | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 50e8255a6..2c2a4b850 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -15,7 +15,6 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
 open Hints
-open Tacexpr
 open Names
 
 DECLARE PLUGIN "g_auto"
@@ -49,10 +48,7 @@ let eval_uconstrs ist cs =
     fail_evar = false;
     expand_evars = true
   } in
-  let map c = { delayed = fun env sigma ->
-    let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in
-    Sigma.Sigma (c, sigma, p)
-  } in
+  let map c env sigma = c env sigma in
   List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
 
 let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 23ce368ee..dd5307638 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -102,18 +102,18 @@ let rec eq_constr_mod_evars sigma x y =
   | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y
 
 let progress_evars t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let check =
-      Proofview.Goal.enter { enter = begin fun gl' ->
+      Proofview.Goal.enter begin fun gl' ->
         let sigma = Tacmach.New.project gl' in
         let newconcl = Proofview.Goal.concl gl' in
         if eq_constr_mod_evars sigma concl newconcl
         then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
         else Proofview.tclUNIT ()
-      end }
+      end
     in t <*> check
-  end }
+  end
 
 TACTIC EXTEND progress_evars
   [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ]
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 5adf8475a..25258ffa9 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -18,7 +18,6 @@ open Glob_term
 open Geninterp
 open Extraargs
 open Tacmach
-open Proofview.Notations
 open Rewrite
 open Stdarg
 open Pcoq.Vernac_
@@ -123,7 +122,7 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
     Tacticals.New.tclMAP
@@ -132,7 +131,7 @@ let clsubstitute o c =
           | Some id when is_tac id -> Tacticals.New.tclIDTAC
           | _ -> cl_rewrite_clause c o AllOccurrences cl)
       (None :: List.map (fun id -> Some id) hyps)
-  end }
+  end
 
 TACTIC EXTEND substitute
 | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 902985827..9446f9df4 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1179,11 +1179,10 @@ let declare_extra_genarg_pprule wit
 
 (** Registering *)
 
-let run_delayed c =
-  Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+let run_delayed c = c (Global.env ()) Evd.empty
 
 let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
-  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g))
+  | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g))
   | clear_flag,ElimOnAnonHyp n as x -> x
   | clear_flag,ElimOnIdent id as x -> x
 
@@ -1203,7 +1202,7 @@ let () =
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
     (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
-    (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c))));
+    (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c))));
   Genprint.register_print0
     wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
@@ -1236,11 +1235,11 @@ let () =
   Genprint.register_print0 wit_bindings
     (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
     (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
+    (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it)));
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
     (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
-    (fun it -> pr_with_bindings pr_econstr pr_leconstr (fst (run_delayed it)));
+    (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it)));
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
     (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f028abde9..68dc1fd37 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -33,7 +33,6 @@ open Environ
 open Termops
 open EConstr
 open Libnames
-open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
@@ -66,9 +65,7 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 let find_global dir s =
   let gr = lazy (find_reference dir s) in
     fun (evd,cstrs) ->
-      let sigma = Sigma.Unsafe.of_evar_map evd in
-      let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
-      let evd = Sigma.to_evar_map sigma in
+      let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in
 	(evd, cstrs), c
 
 (** Utility for dealing with polymorphic applications *)
@@ -89,9 +86,7 @@ let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
   let s = Typeclasses.set_resolvable Evd.Store.empty false in
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in
-  let evd' = Sigma.to_evar_map evd' in
+  let (evd', t) = Evarutil.new_evar ~store:s env evd t in
   let ev, _ = destEvar evd' t in
     (evd', Evar.Set.add ev cstrs), t
 
@@ -176,17 +171,13 @@ end) = struct
   let proper_type = 
     let l = lazy (Lazy.force proper_class).cl_impl in
       fun (evd,cstrs) -> 
-        let sigma = Sigma.Unsafe.of_evar_map evd in
-        let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
-        let evd = Sigma.to_evar_map sigma in
+        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
 	  (evd, cstrs), c
 	
   let proper_proxy_type = 
     let l = lazy (Lazy.force proper_proxy_class).cl_impl in
       fun (evd,cstrs) -> 
-        let sigma = Sigma.Unsafe.of_evar_map evd in
-        let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
-        let evd = Sigma.to_evar_map sigma in
+        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
 	  (evd, cstrs), c
 
   let proper_proof env evars carrier relation x =
@@ -357,9 +348,7 @@ end) = struct
 	  (try
 	   let params, args = Array.chop (Array.length args - 2) args in
 	   let env' = push_rel_context rels env in
-	   let sigma = Sigma.Unsafe.of_evar_map sigma in
-	   let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
-	   let evars = Sigma.to_evar_map evars in
+	   let (evars, (evar, _)) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
 	   let evars, inst = 
 	     app_poly env (evars,Evar.Set.empty)
 	       rewrite_relation_class [| evar; mkApp (c, params) |] in
@@ -419,9 +408,7 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let sigma = Sigma.Unsafe.of_evar_map evd in
-    let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in
-    let evd = Sigma.to_evar_map sigma in
+    let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
@@ -751,9 +738,9 @@ let default_flags = { under_lambdas = true; on_morphisms = true; }
 
 let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
 
-let new_global (evars, cstrs) gr = 
-  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr
-  in (Sigma.to_evar_map sigma, cstrs), c
+let new_global (evars, cstrs) gr =
+  let (sigma,c) = Evarutil.new_global evars gr in
+  (sigma, cstrs), c
 
 let make_eq sigma =
   new_global sigma (Coqlib.build_coq_eq ())
@@ -1406,15 +1393,14 @@ module Strategies =
     let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
 	fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
           let rfn, ckind = Redexpr.reduction_of_red_expr env r in
-          let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in
-	  let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in
-	  let evars' = Sigma.to_evar_map sigma in
-	    if Termops.eq_constr evars' t' t then
+          let sigma = goalevars evars in
+	  let (sigma, t') = rfn env sigma t in
+	    if Termops.eq_constr sigma t' t then
 	      state, Identity
 	    else
 	      state, Success { rew_car = ty; rew_from = t; rew_to = t';
 			       rew_prf = RewCast ckind; 
-			       rew_evars = evars', cstrevars evars }
+			       rew_evars = sigma, cstrevars evars }
 							   }
 	
     let fold_glob c : 'a pure_strategy = { strategy =
@@ -1541,7 +1527,7 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with
     insert_dependent env sigma decl (ndecl :: accu) rem
 
 let assert_replacing id newt tac = 
-  let prf = Proofview.Goal.enter { enter = begin fun gl ->
+  let prf = Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -1552,17 +1538,17 @@ let assert_replacing id newt tac =
     | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
-    Refine.refine ~unsafe:false { run = begin fun sigma ->
-      let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
-      let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
+    Refine.refine ~unsafe:false begin fun sigma ->
+      let (sigma, ev) = Evarutil.new_evar env' sigma concl in
+      let (sigma, ev') = Evarutil.new_evar env sigma newt in
       let map d =
         let n = NamedDecl.get_id d in
         if Id.equal n id then ev' else mkVar n
       in
-      let (e, _) = destEvar (Sigma.to_evar_map sigma) ev in
-      Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
-    end }
-  end } in
+      let (e, _) = destEvar sigma ev in
+      (sigma, mkEvar (e, Array.map_of_list map nc))
+    end
+  end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
 
 let newfail n s = 
@@ -1586,7 +1572,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	match clause, prf with
 	| Some id, Some p ->
             let tac = tclTHENLIST [
-              Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h };
+              Refine.refine ~unsafe:false (fun h -> (h,p));
               Proofview.Unsafe.tclNEWGOALS gls;
             ] in
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1597,19 +1583,19 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
-            Proofview.Goal.enter { enter = begin fun gl ->
+            Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
-            let make = { run = begin fun sigma ->
-              let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
-              Sigma (mkApp (p, [| ev |]), sigma, q)
-            end } in
+            let make = begin fun sigma ->
+              let (sigma, ev) = Evarutil.new_evar env sigma newt in
+              (sigma, mkApp (p, [| ev |]))
+            end in
             Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
-            end }
+            end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
             convert_concl_no_check newt DEFAULTcast
   in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
@@ -1637,7 +1623,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
     with
     | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
       raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
-  end }
+  end
 
 let tactic_init_setoid () = 
   try init_setoid (); Proofview.tclUNIT ()
@@ -2092,7 +2078,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 
 (** Setoid rewriting when called with "rewrite" *)
 let general_s_rewrite cl l2r occs (c,l) ~new_goals =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
   let unify env evars t = unify_abs res l2r sort env evars t in
   let app = apply_rule unify occs in
@@ -2114,7 +2100,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
     | RewriteFailure e ->
       tclFAIL 0 (str"setoid rewrite failed: " ++ e)
     | e -> Proofview.tclZERO ~info e)
-  end }
+  end
 
 let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
 
@@ -2126,7 +2112,7 @@ let not_declared env sigma ty rel =
      str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
 let setoid_proof ty fn fallback =
-  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
@@ -2155,7 +2141,7 @@ let setoid_proof ty fn fallback =
                 | e' -> Proofview.tclZERO ~info e'
               end
       end
-  end }
+  end
 
 let tac_open ((evm,_), c) tac = 
     (tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c))
@@ -2195,7 +2181,7 @@ let setoid_transitivity c =
     
 let setoid_symmetry_in id =
   let open Tacmach.New in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
@@ -2212,7 +2198,7 @@ let setoid_symmetry_in id =
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
       (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
-  end }
+  end
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index b78dc3742..cfb698cd8 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -117,8 +117,7 @@ type open_glob_constr = unit * glob_constr_and_expr
 type binding_bound_vars = Constr_matching.binding_bound_vars
 type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
 
-type 'a delayed_open = 'a Tactypes.delayed_open =
-  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
 
 type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 37fdd185e..ff76d06cf 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -37,7 +37,6 @@ open Misctypes
 open Locus
 open Tacintern
 open Taccoerce
-open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
@@ -767,9 +766,7 @@ let interp_may_eval f ist env sigma = function
       let (sigma,redexp) = interp_red_expr ist env sigma r in
       let (sigma,c_interp) = f ist env sigma c in
       let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
-      let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in
-      (Sigma.to_evar_map sigma, c)
+      redfun env sigma c_interp
   | ConstrContext ((loc,s),c) ->
       (try
 	let (sigma,ic) = f ist env sigma c in
@@ -829,12 +826,12 @@ let rec message_of_value v =
     Ftactic.return (str "<tactic>")
   else if has_type v (topwit wit_constr) then
     let v = out_gen (topwit wit_constr) v in
-    Ftactic.enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
+    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end
   else if has_type v (topwit wit_constr_under_binders) then
     let c = out_gen (topwit wit_constr_under_binders) v in
-    Ftactic.enter { enter = begin fun gl ->
+    Ftactic.enter begin fun gl ->
       Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
-    end }
+    end
   else if has_type v (topwit wit_unit) then
     Ftactic.return (str "()")
   else if has_type v (topwit wit_int) then
@@ -842,24 +839,24 @@ let rec message_of_value v =
   else if has_type v (topwit wit_intro_pattern) then
     let p = out_gen (topwit wit_intro_pattern) v in
     let print env sigma c =
-      let (c, sigma) = Tactics.run_delayed env sigma c in
+      let (sigma, c) = c env sigma in
       pr_econstr_env env sigma c
     in
-    Ftactic.enter { enter = begin fun gl ->
+    Ftactic.enter begin fun gl ->
       Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
-    end }
+    end
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
-    Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
+    Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end
   else if has_type v (topwit wit_uconstr) then
     let c = out_gen (topwit wit_uconstr) v in
-    Ftactic.enter { enter = begin fun gl ->
+    Ftactic.enter begin fun gl ->
       Ftactic.return (pr_closed_glob_env (pf_env gl)
                         (project gl) c)
-    end }
+    end
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
-    Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
+    Ftactic.enter begin fun gl -> Ftactic.return (pr_id id) end
   else match Value.to_list v with
   | Some l ->
     Ftactic.List.map message_of_value l >>= fun l ->
@@ -905,11 +902,7 @@ and interp_intro_pattern_action ist env sigma = function
       let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
       sigma, IntroInjection l
   | IntroApplyOn ((loc,c),ipat) ->
-      let c = { delayed = fun env sigma ->
-        let sigma = Sigma.to_evar_map sigma in
-        let (sigma, c) = interp_open_constr ist env sigma c in
-        Sigma.Unsafe.of_pair (c, sigma)
-      } in
+      let c env sigma = interp_open_constr ist env sigma c in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
       sigma, IntroApplyOn ((loc,c),ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
@@ -1003,21 +996,15 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
   let loc2 = loc_of_bindings bl in
   let loc  = Loc.merge_opt loc1 loc2 in
-  let f = { delayed = fun env sigma ->
-    let sigma = Sigma.to_evar_map sigma in
-    let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in
-    Sigma.Unsafe.of_pair (c, sigma)
-  } in
-    (loc,f)
+  let f env sigma = interp_open_constr_with_bindings ist env sigma cb in
+  (loc,f)
 
 let interp_destruction_arg ist gl arg =
   match arg with
   | keep,ElimOnConstr c ->
-      keep,ElimOnConstr { delayed = fun env sigma ->
-        let sigma = Sigma.to_evar_map sigma in
-        let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in
-        Sigma.Unsafe.of_pair (c, sigma)
-      }
+      keep,ElimOnConstr begin fun env sigma ->
+        interp_open_constr_with_bindings ist env sigma c
+      end
   | keep,ElimOnAnonHyp n as x -> x
   | keep,ElimOnIdent (loc,id) ->
       let error () = user_err ?loc 
@@ -1028,12 +1015,12 @@ let interp_destruction_arg ist gl arg =
         if Tactics.is_quantified_hypothesis id' gl
         then keep,ElimOnIdent (loc,id')
         else
-          (keep, ElimOnConstr { delayed = begin fun env sigma ->
-          try Sigma.here (constr_of_id env id', NoBindings) sigma
+          (keep, ElimOnConstr begin fun env sigma ->
+          try (sigma, (constr_of_id env id', NoBindings))
           with Not_found ->
             user_err ?loc  ~hdr:"interp_destruction_arg" (
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
-          end })
+          end)
       in
       try
         (** FIXME: should be moved to taccoerce *)
@@ -1051,18 +1038,17 @@ let interp_destruction_arg ist gl arg =
           keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
         else match Value.to_constr v with
         | None -> error ()
-        | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) }
+        | Some c -> keep,ElimOnConstr (fun env sigma -> (sigma, (c,NoBindings)))
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
           let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
-          let f = { delayed = fun env sigma ->
-            let sigma = Sigma.to_evar_map sigma in
+          let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
-            Sigma.Unsafe.of_pair ((c,NoBindings), sigma)
-          } in
+            (sigma, (c,NoBindings))
+          in
           keep,ElimOnConstr f
 
 (* Associates variables with values and gives the remaining variables and
@@ -1198,9 +1184,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
            tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
          end
   | TacAbstract (tac,ido) ->
-      Proofview.Goal.enter { enter = begin fun gl -> Tactics.tclABSTRACT
+      Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
         (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
-      end }
+      end
   | TacThen (t1,t) ->
       Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
   | TacDispatch tl ->
@@ -1318,12 +1304,13 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
   | TacGeneric arg -> interp_genarg ist arg
   | Reference r -> interp_ltac_reference false ist r
   | ConstrMayEval c ->
-      Ftactic.s_enter { s_enter = begin fun gl ->
+      Ftactic.enter begin fun gl ->
         let sigma = project gl in
         let env = Proofview.Goal.env gl in
         let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
-        Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma)
-      end }
+        Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Ftactic.return (Value.of_constr c_interp))
+      end
   | TacCall (loc,(r,[])) ->
       interp_ltac_reference true ist r
   | TacCall (loc,(f,l)) ->
@@ -1332,18 +1319,19 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
       Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
       interp_app loc ist fv largs
   | TacFreshId l ->
-      Ftactic.enter { enter = begin fun gl ->
+      Ftactic.enter begin fun gl ->
         let id = interp_fresh_id ist (pf_env gl) (project gl) l in
         Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id)))
-      end }
+      end
   | TacPretype c ->
-      Ftactic.s_enter { s_enter = begin fun gl ->
+      Ftactic.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        let c = interp_uconstr ist env (Sigma.to_evar_map sigma) c in
-        let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in
-        Sigma (Ftactic.return (Value.of_constr c), sigma, p)
-      end }
+        let c = interp_uconstr ist env sigma c in
+        let (sigma, c) = type_uconstr ist c env sigma in
+        Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Ftactic.return (Value.of_constr c))
+      end
   | TacNumgoals ->
       Ftactic.lift begin
         let open Proofview.Notations in
@@ -1504,16 +1492,16 @@ and interp_match ist lz constr lmr =
           Proofview.tclZERO ~info e
     end
   end >>= fun constr ->
-  Ftactic.enter { enter = begin fun gl ->
+  Ftactic.enter begin fun gl ->
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
     let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
     interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr)
-  end }
+  end
 
 (* Interprets the Match Context expressions *)
 and interp_match_goal ist lz lr lmr =
-    Ftactic.enter { enter = begin fun gl ->
+    Ftactic.enter begin fun gl ->
       let sigma = project gl in
       let env = Proofview.Goal.env gl in
       let hyps = Proofview.Goal.hyps gl in
@@ -1521,7 +1509,7 @@ and interp_match_goal ist lz lr lmr =
       let concl = Proofview.Goal.concl gl in
       let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
       interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr)
-    end }
+    end
 
 (* Interprets extended tactic generic arguments *)
 and interp_genarg ist x : Val.t Ftactic.t =
@@ -1558,24 +1546,25 @@ and interp_genarg ist x : Val.t Ftactic.t =
     independently of goals. *)
 
 and interp_genarg_constr_list ist x =
-  Ftactic.nf_s_enter { s_enter = begin fun gl ->
+  Ftactic.nf_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 lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
   let (sigma,lc) = interp_constr_list ist env sigma lc in
   let lc = in_list (val_tag wit_constr) lc in
-  Sigma.Unsafe.of_pair (Ftactic.return lc, sigma)
-  end }
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (Ftactic.return lc)
+  end
 
 and interp_genarg_var_list ist x =
-  Ftactic.enter { enter = begin fun gl ->
+  Ftactic.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 lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
   let lc = interp_hyp_list ist env sigma lc in
   let lc = in_list (val_tag wit_var) lc in
   Ftactic.return lc
-  end }
+  end
 
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist e : EConstr.t Ftactic.t =
@@ -1584,7 +1573,7 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
       (val_interp ist e)
       begin function (err, info) -> match err with
         | Not_found ->
-            Ftactic.enter { enter = begin fun gl ->
+            Ftactic.enter begin fun gl ->
               let env = Proofview.Goal.env gl in
               Proofview.tclLIFT begin
                 debugging_step ist (fun () ->
@@ -1592,11 +1581,11 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
                     Pptactic.pr_glob_tactic env e)
               end
             <*> Proofview.tclZERO Not_found
-            end }
+            end
         | err -> Proofview.tclZERO ~info err
       end
   end >>= fun result ->
-  Ftactic.enter { enter = begin fun gl ->
+  Ftactic.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = project gl in
   let result = Value.normalize result in
@@ -1613,7 +1602,7 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
     let env = Proofview.Goal.env gl in
     Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
       str "offending expression: " ++ fnl() ++ pr_inspect env e result)
-  end }
+  end
 
 
 (* Interprets tactic expressions : returns a "tactic" *)
@@ -1635,7 +1624,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   match tac with
   (* Basic tactics *)
   | TacIntroPattern (ev,l) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
@@ -1645,11 +1634,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (* spiwack: print uninterpreted, not sure if it is the
              expected behaviour. *)
           (Tactics.intro_patterns ev l')) sigma
-      end }
+      end
   | TacApply (a,ev,cb,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
 	let l = List.map (fun (k,c) ->
@@ -1662,10 +1651,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
               let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in
               sigma, Tactics.apply_delayed_in a ev id l cl in
         Tacticals.New.tclWITHHOLES ev tac sigma
-      end }
+      end
       end
   | TacElim (ev,(keep,cb),cbo) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in 
         let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
@@ -1675,9 +1664,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
           name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
         in
         Tacticals.New.tclWITHHOLES ev named_tac sigma
-      end }
+      end
   | TacCase (ev,(keep,cb)) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let sigma = project gl in
         let env = Proofview.Goal.env gl in
         let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
@@ -1686,11 +1675,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
           name_atomic ~env (TacCase(ev,(keep,cb))) tac
         in
         Tacticals.New.tclWITHHOLES ev named_tac sigma
-      end }
+      end
   | TacMutualFix (id,n,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+      Proofview.Goal.nf_enter begin fun gl ->
         let env = pf_env gl in
         let f sigma (id,n,c) =
           let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1698,14 +1687,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in
-        Sigma.Unsafe.of_pair (tac, sigma)
-      end }
+        Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0)
+      end
       end
   | TacMutualCofix (id,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+      Proofview.Goal.nf_enter begin fun gl ->
         let env = pf_env gl in
         let f sigma (id,c) =
 	  let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1713,12 +1702,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in
-        Sigma.Unsafe.of_pair (tac, sigma)
-      end }
+        Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0)
+      end
       end
   | TacAssert (ev,b,t,ipat,c) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let (sigma,c) =
@@ -1733,9 +1722,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (name_atomic ~env
           (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c))
           (Tactics.forward b tac ipat' c)) sigma
-      end }
+      end
   | TacGeneralize cl ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let sigma = project gl in
         let env = Proofview.Goal.env gl in
         let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
@@ -1743,9 +1732,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (name_atomic ~env
           (TacGeneralize cl)
           (Tactics.generalize_gen cl)) sigma
-      end }
+      end
   | TacLetTac (ev,na,c,clp,b,eqpat) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let clp = interp_clause ist env sigma clp in
@@ -1777,13 +1766,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	    (Tacticals.New.tclWITHHOLES ev
                (let_pat_tac b (interp_name ist env sigma na)
                   (sigma,c) clp eqpat) sigma')
-      end }
+      end
 
   (* Derived basic tactics *)
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
          prenormalised. *)
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+      Proofview.Goal.nf_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let sigma,l =
@@ -1802,23 +1791,23 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let l,lp = List.split l in
         let sigma,el =
           Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in
-        let tac = name_atomic ~env
+        Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (name_atomic ~env
           (TacInductionDestruct(isrec,ev,(lp,el)))
-            (Tactics.induction_destruct isrec ev (l,el))
-        in
-        Sigma.Unsafe.of_pair (tac, sigma)
-      end }
+            (Tactics.induction_destruct isrec ev (l,el)))
+      end
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+      Proofview.Goal.nf_enter begin fun gl ->
         let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
-        Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma)
-      end }
+        Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
+      end
   | TacChange (None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let is_onhyps = match cl.onhyps with
           | None | Some [] -> true
           | _ -> false
@@ -1827,58 +1816,50 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp patvars = { Sigma.run = begin fun sigma ->
+        let c_interp patvars sigma =
 	  let lfun' = Id.Map.fold (fun id c lfun ->
 	    Id.Map.add id (Value.of_constr c) lfun) 
 	    patvars ist.lfun
 	  in
-	  let sigma = Sigma.to_evar_map sigma in
 	  let ist = { ist with lfun = lfun' } in
-	  let (sigma, c) =
             if is_onhyps && is_onconcl
             then interp_type ist (pf_env gl) sigma c
             else interp_constr ist (pf_env gl) sigma c
-          in
-          Sigma.Unsafe.of_pair (c, sigma)
-        end } in
+        in
         Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
-      end }
+      end
       end
   | TacChange (Some op,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let op = interp_typed_pattern ist env sigma op in
         let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
-        let c_interp patvars = { Sigma.run = begin fun sigma ->
+        let c_interp patvars sigma =
           let lfun' = Id.Map.fold (fun id c lfun ->
             Id.Map.add id (Value.of_constr c) lfun) 
             patvars ist.lfun
           in
           let ist = { ist with lfun = lfun' } in
             try
-              let sigma = Sigma.to_evar_map sigma in
-              let (sigma, c) = interp_constr ist env sigma c in
-              Sigma.Unsafe.of_pair (c, sigma)
+              interp_constr ist env sigma c
             with e when to_catch e (* Hack *) ->
               user_err  (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
-        end } in
+        in
         Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
-      end }
+      end
       end
 
 
   (* Equality and inversion *)
   | TacRewrite (ev,l,cl,by) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let l' = List.map (fun (b,m,(keep,c)) ->
-          let f = { delayed = fun env sigma ->
-            let sigma = Sigma.to_evar_map sigma in
-            let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in
-            Sigma.Unsafe.of_pair (c, sigma)
-          } in
+          let f env sigma =
+            interp_open_constr_with_bindings ist env sigma c
+          in
 	  (b,m,keep,f)) l in
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
@@ -1889,9 +1870,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
              (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by),
                Equality.Naive)
                 by))
-      end }
+      end
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let (sigma,c_interp) =
@@ -1907,9 +1888,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (name_atomic ~env
           (TacInversion(DepInversion(k,c_interp,ids),dqhyps))
           (Inv.dinv k c_interp ids_interp dqhyps)) sigma
-      end }
+      end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
-      Proofview.Goal.enter { enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let hyps = interp_hyp_list ist env sigma idl in
@@ -1919,20 +1900,19 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (name_atomic ~env
           (TacInversion (NonDepInversion (k,hyps,ids),dqhyps))
           (Inv.inv_clause k ids_interp hyps dqhyps)) sigma
-      end }
+      end
   | TacInversion (InversionUsing (c,idl),hyp) ->
-      Proofview.Goal.s_enter { s_enter = begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let (sigma,c_interp) = interp_constr ist env sigma c in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let hyps = interp_hyp_list ist env sigma idl in
-        let tac = name_atomic ~env
+        Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+        (name_atomic ~env
           (TacInversion (InversionUsing (c_interp,hyps),dqhyps))
-          (Leminv.lemInv_clause dqhyps c_interp hyps)
-        in
-        Sigma.Unsafe.of_pair (tac, sigma)
-      end }
+          (Leminv.lemInv_clause dqhyps c_interp hyps))
+      end
 
 (* Initial call for interpretation *)
 
@@ -1953,7 +1933,7 @@ let eval_tactic_ist ist t =
 
 
 let interp_tac_gen lfun avoid_ids debug t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
@@ -1961,7 +1941,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
     (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
-  end }
+  end
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
 
@@ -1980,9 +1960,9 @@ let hide_interp global t ot =
     Proofview.tclENV >>= fun env ->
     hide_interp env
   else
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       hide_interp (Proofview.Goal.env gl)
-    end }
+    end
 
 (***************************************************************************)
 (** Register standard arguments *)
@@ -2015,37 +1995,35 @@ let () =
 let () =
   declare_uniform wit_string
 
-let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl ->
+let lift f = (); fun ist x -> Ftactic.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
   Ftactic.return (f ist env sigma x)
-end }
+end
 
-let lifts f = (); fun ist x -> Ftactic.nf_s_enter { s_enter = begin fun gl ->
+let lifts f = (); fun ist x -> Ftactic.nf_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, v) = f ist env sigma x in
-  Sigma.Unsafe.of_pair (Ftactic.return v, sigma)
-end }
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (Ftactic.return v)
+end
 
-let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma ->
-  let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in
-  Sigma.Unsafe.of_pair (bl, sigma)
-  }
+let interp_bindings' ist bl = Ftactic.return begin fun env sigma ->
+  interp_bindings ist env sigma bl
+  end
 
-let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma ->
-  let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in
-  Sigma.Unsafe.of_pair (c, sigma)
-  }
+let interp_constr_with_bindings' ist c = Ftactic.return begin fun env sigma ->
+  interp_constr_with_bindings ist env sigma c
+  end
 
-let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma ->
-  let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in
-  Sigma.Unsafe.of_pair (c, sigma)
-  }
+let interp_open_constr_with_bindings' ist c = Ftactic.return begin fun env sigma ->
+  interp_open_constr_with_bindings ist env sigma c
+  end
 
-let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl ->
+let interp_destruction_arg' ist c = Ftactic.enter begin fun gl ->
   Ftactic.return (interp_destruction_arg ist gl c)
-end }
+end
 
 let interp_pre_ident ist env sigma s =
   s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string
@@ -2078,9 +2056,9 @@ let () =
   register_interp0 wit_ltac interp
 
 let () =
-  register_interp0 wit_uconstr (fun ist c -> Ftactic.enter { enter = begin fun gl ->
+  register_interp0 wit_uconstr (fun ist c -> Ftactic.enter begin fun gl ->
     Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c)
-  end })
+  end)
 
 (***************************************************************************)
 (* Other entry points *)
@@ -2111,7 +2089,7 @@ let _ =
 let dummy_id = Id.of_string "_"
 
 let lift_constr_tac_to_ml_tac vars tac =
-  let tac _ ist = Proofview.Goal.enter { enter = begin fun gl ->
+  let tac _ ist = Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = project gl in
     let map = function
@@ -2124,7 +2102,7 @@ let lift_constr_tac_to_ml_tac vars tac =
     in
     let args = List.map_filter map vars in
     tac args ist
-  end } in
+  end in
   tac
 
 let vernac_debug b =
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 294cba4d7..e6d0370f3 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -12,7 +12,6 @@ open Pp
 open Tacexpr
 open Termops
 open Nameops
-open Proofview.Notations
 
 
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
@@ -57,10 +56,10 @@ let db_pr_goal gl =
                    str" "  ++ pc) ++ fnl ()
 
 let db_pr_goal =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let pg = db_pr_goal gl in
   Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
-  end }
+  end
 
 
 (* Prints the commands *)