From 954fbd3b102060ed1e2122f571a430f05a174e42 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 May 2017 22:14:35 +0200
Subject: 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.
---
 plugins/btauto/refl_btauto.ml                  |  10 +-
 plugins/cc/cctac.ml                            |  69 +++---
 plugins/firstorder/g_ground.ml4                |  11 +-
 plugins/firstorder/ground.ml                   |   9 +-
 plugins/firstorder/instances.ml                |  32 ++-
 plugins/firstorder/rules.ml                    |  32 +--
 plugins/fourier/fourierR.ml                    |   4 +-
 plugins/funind/functional_principles_proofs.ml |   2 +-
 plugins/funind/functional_principles_types.ml  |   5 +-
 plugins/funind/g_indfun.ml4                    |   3 +-
 plugins/funind/indfun.ml                       |   3 +-
 plugins/funind/recdef.ml                       |  11 +-
 plugins/ltac/coretactics.ml4                   |  12 +-
 plugins/ltac/evar_tactics.ml                   |  19 +-
 plugins/ltac/extratactics.ml4                  |  73 +++----
 plugins/ltac/g_auto.ml4                        |   6 +-
 plugins/ltac/g_class.ml4                       |   8 +-
 plugins/ltac/g_rewrite.ml4                     |   5 +-
 plugins/ltac/pptactic.ml                       |  11 +-
 plugins/ltac/rewrite.ml                        |  86 +++-----
 plugins/ltac/tacexpr.mli                       |   3 +-
 plugins/ltac/tacinterp.ml                      | 292 ++++++++++++-------------
 plugins/ltac/tactic_debug.ml                   |   5 +-
 plugins/micromega/coq_micromega.ml             |  18 +-
 plugins/omega/coq_omega.ml                     |  71 +++---
 plugins/quote/quote.ml                         |  16 +-
 plugins/romega/const_omega.ml                  |   2 +-
 plugins/romega/const_omega.mli                 |   2 +-
 plugins/romega/refl_omega.ml                   |   6 +-
 plugins/setoid_ring/newring.ml                 |   8 +-
 30 files changed, 379 insertions(+), 455 deletions(-)

(limited to 'plugins')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 33a9dd4fd9..6281b2675e 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,5 +1,3 @@
-open Proofview.Notations
-
 let contrib_name = "btauto"
 
 let init_constant dir s =
@@ -219,7 +217,7 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
       let concl = EConstr.Unsafe.to_constr concl in
@@ -232,10 +230,10 @@ module Btauto = struct
       | _ ->
           let msg = str "Btauto: Internal error" in
           Tacticals.New.tclFAIL 0 msg
-    end }
+    end
 
   let tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let concl = EConstr.Unsafe.to_constr concl in
       let sigma = Tacmach.New.project gl in
@@ -262,6 +260,6 @@ module Btauto = struct
       | _ ->
           let msg = str "Cannot recognize a boolean equality" in
           Tacticals.New.tclFAIL 0 msg
-    end }
+    end
 
 end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 43c06a54d4..b638f23606 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -241,24 +241,20 @@ let app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc -> k (mkApp (fc, args))
 
 let rec gen_holes env sigma t n accu =
-  let open Sigma in
   if Int.equal n 0 then (sigma, List.rev accu)
   else match EConstr.kind sigma t with
   | Prod (_, u, t) ->
-    let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (ev, sigma, _) = Evarutil.new_evar env sigma u in
-    let sigma = Sigma.to_evar_map sigma in
+    let (sigma, ev) = Evarutil.new_evar env sigma u in
     let t = EConstr.Vars.subst1 ev t in
     gen_holes env sigma t (pred n) (ev :: accu)
   | _ -> assert false
 
 let app_global_with_holes f args n =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    Refine.refine { Sigma.run = begin fun sigma ->
-      let sigma = Sigma.to_evar_map sigma in
+    Refine.refine begin fun sigma ->
       let t = Tacmach.New.pf_get_type_of gl fc in
       let t = Termops.prod_applist sigma t (Array.to_list args) in
       let ans = mkApp (fc, args) in
@@ -266,32 +262,33 @@ let app_global_with_holes f args n =
       let ans = applist (ans, holes) in
       let evdref = ref sigma in
       let () = Typing.e_check env evdref ans concl in
-      Sigma.Unsafe.of_pair (ans, !evdref)
-    end }
-  end }
+      (!evdref, ans)
+    end
+  end
 
 let assert_before n c =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
-    Sigma.Unsafe.of_pair (assert_before n c, evm)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm)
+    (assert_before n c)
+  end
 
 let refresh_type env evm ty =
   Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
 			      (Some false) env evm ty
 
 let refresh_universes ty k =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
     let evm, ty = refresh_type env evm ty in
-    Sigma.Unsafe.of_pair (k ty, evm)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty)
+  end
 
 let constr_of_term c = EConstr.of_constr (constr_of_term c)
 
 let rec proof_tac p : unit Proofview.tactic =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
   try (* type_of can raise exceptions *)
   match p.p_rule with
@@ -354,10 +351,10 @@ let rec proof_tac p : unit Proofview.tactic =
 	 Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
                                (Tacticals.New.tclTHEN injt (proof_tac prf))))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end
 
 let refute_tac c t1 t2 p =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
@@ -366,16 +363,16 @@ let refute_tac c t1 t2 p =
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
-  end }
+  end
 
 let refine_exact_check c =
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
-    Sigma.Unsafe.of_pair (exact_check c, evm)
-  end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (exact_check c)
+  end
 
 let convert_to_goal_tac c t1 t2 p = 
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let k sort =
     let neweq= app_global _eq [|sort;tt1;tt2|] in
@@ -386,21 +383,21 @@ let convert_to_goal_tac c t1 t2 p =
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
 			   [proof_tac p; endt refine_exact_check]
   in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
-  end }
+  end
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let tt2=constr_of_term t2 in
   let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in
   let false_t=mkApp (c2,[|mkVar h|]) in
     Tacticals.New.tclTHENS (assert_before (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
        simplest_elim false_t]
-  end }
+  end
 
 (* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
 let discriminate_tac cstru p =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
@@ -410,7 +407,7 @@ let discriminate_tac cstru p =
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; Equality.discrHyp hid])
-  end }
+  end
 
 (* wrap everything *)
 
@@ -421,7 +418,7 @@ let build_term_to_complete uf pac =
   (applist (mkConstructU (kn, EInstance.make u), real_args), pac.arity)
 
 let cc_tactic depth additionnal_terms =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library Coqlib.logic_module_name;
     let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
@@ -477,7 +474,7 @@ let cc_tactic depth additionnal_terms =
                 let ida = EConstr.of_constr ida in
                 let idb = EConstr.of_constr idb in
 		convert_to_hyp_tac ida ta idb tb p
-  end }
+  end
 
 let cc_fail =
   Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
@@ -500,17 +497,17 @@ let congruence_tac depth l =
 
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) >>= fun fc ->
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm term in
-    Sigma.Unsafe.of_pair (k term, evm)
-    end }
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k term)
+    end
 
 let f_equal =
-  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 cut_eq c1 c2 =
@@ -537,4 +534,4 @@ let f_equal =
         | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT ()
         | e -> Proofview.tclZERO ~info e
       end
-  end }
+  end
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index bbb9feae2e..e3fab6d012 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,7 +15,6 @@ open Ground
 open Goptions
 open Tacmach.New
 open Tacticals.New
-open Proofview.Notations
 open Tacinterp
 open Libnames
 open Stdarg
@@ -84,24 +83,24 @@ let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 let gen_ground_tac flag taco ids bases =
   let backup= !qflag in
   Proofview.tclOR begin
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
       qflag:=flag;
       let solver=
 	match taco with
 	    Some tac-> tac
 	  | None-> snd (default_solver ()) in
       let startseq k =
-        Proofview.Goal.s_enter { s_enter = begin fun gl ->
+        Proofview.Goal.enter begin fun gl ->
 	let seq=empty_seq !ground_depth in
         let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
         let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
-        Sigma.Unsafe.of_pair (k seq, sigma)
-        end }
+        tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
+        end
       in
       let result=ground_tac solver startseq in
       qflag := backup;
       result
-  end }
+  end
   end
   (fun (e, info) -> qflag := backup; Proofview.tclZERO ~info e)
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index ab1dd07c11..0fa3089e73 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -14,7 +14,6 @@ open Instances
 open Term
 open Tacmach.New
 open Tacticals.New
-open Proofview.Notations
 
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
@@ -31,10 +30,10 @@ let update_flags ()=
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   update_flags ();
   let rec toptac skipped seq =
-    Proofview.Goal.enter { enter = begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
     let () =
       if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
       then
@@ -127,7 +126,7 @@ let ground_tac solver startseq =
 		  end
 	    with Heap.EmptyHeap->solver
       end
-    end } in
+    end in
     let n = List.length (Proofview.Goal.hyps gl) in
     startseq (fun seq -> wrap n true (toptac []) seq)
-  end }
+  end
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 04bca584f3..e1d765a420 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -21,7 +21,6 @@ open Formula
 open Sequent
 open Names
 open Misctypes
-open Sigma.Notations
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
@@ -114,9 +113,7 @@ let mk_open_instance env evmap id idc m t =
   let rec aux n avoid env evmap decls =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id_in_env avoid var_id env) in
-      let evmap = Sigma.Unsafe.of_evar_map evmap in
-      let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let evmap = Sigma.to_evar_map evmap in
+      let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
       let decl = LocalAssum (Name nid, c) in
 	aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
@@ -126,7 +123,7 @@ let mk_open_instance env evmap id idc m t =
 
 let left_instance_tac (inst,id) continue seq=
   let open EConstr in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   match inst with
       Phantom dom->
@@ -137,10 +134,10 @@ let left_instance_tac (inst,id) continue seq=
 	    [tclTHENLIST
 	       [introf;
                 (pf_constr_of_global id >>= fun idc ->
-                Proofview.Goal.enter { enter = begin fun gl ->
+                Proofview.Goal.enter begin fun gl ->
                   let id0 = List.nth (pf_ids_of_hyps gl) 0 in
                   generalize [mkApp(idc, [|mkVar id0|])]
-                end });
+                end);
 		introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -153,7 +150,7 @@ let left_instance_tac (inst,id) continue seq=
 	  let special_generalize=
 	    if m>0 then
 	      (pf_constr_of_global id >>= fun idc ->
-		Proofview.Goal.s_enter { s_enter = begin fun gl->
+		Proofview.Goal.enter begin fun gl->
 		  let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
@@ -162,8 +159,9 @@ let left_instance_tac (inst,id) continue seq=
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
-		    Sigma.Unsafe.of_pair (generalize [gt], evmap)
-                end })
+                  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap)
+		    (generalize [gt])
+                end)
 	    else
 	      pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
 	  in
@@ -172,20 +170,20 @@ let left_instance_tac (inst,id) continue seq=
 	       introf;
 	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
-  end }
+  end
 
 let right_instance_tac inst continue seq=
   let open EConstr in
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   match inst with
       Phantom dom ->
 	tclTHENS (cut dom)
 	[tclTHENLIST
 	   [introf;
-            Proofview.Goal.enter { enter = begin fun gl ->
+            Proofview.Goal.enter begin fun gl ->
               let id0 = List.nth (pf_ids_of_hyps gl) 0 in
               split (ImplicitBindings [mkVar id0])
-            end };
+            end;
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
@@ -193,7 +191,7 @@ let right_instance_tac inst continue seq=
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
-  end }
+  end
 
 let instance_tac inst=
   if (snd inst)==dummy_id then
@@ -202,9 +200,9 @@ let instance_tac inst=
     left_instance_tac inst
 
 let quantified_tac lf backtrack continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let insts=give_instances (project gl) lf seq in
     tclORELSE
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
       backtrack
-  end }
+  end
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f745dbeb4b..b7fe25a32a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -32,7 +32,7 @@ type lseqtac= global_reference -> seqtac
 type 'a with_backtracking = tactic -> 'a
 
 let wrap n b continue seq =
-  Proofview.Goal.nf_enter { enter = begin fun gls ->
+  Proofview.Goal.nf_enter begin fun gls ->
   Control.check_for_interrupt ();
   let nc = Proofview.Goal.hyps gls in
   let env=pf_env gls in
@@ -52,7 +52,7 @@ let wrap n b continue seq =
   let seq2=if b then
     add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
     continue seq2
-  end }
+  end
 
 let basename_of_global=function
     VarRef id->id
@@ -65,12 +65,12 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   try
     pf_constr_of_global (find_left (project gl) t seq) >>= fun c ->
     exact_no_check c
   with Not_found -> tclFAIL 0 (Pp.str "No axiom link")
-  end }
+  end
 
 let ll_atom_tac a backtrack id continue seq =
   let open EConstr in
@@ -107,7 +107,7 @@ let arrow_tac backtrack continue seq=
 (* left connectives rules *)
 
 let left_and_tac ind backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let n=(construct_nhyps (pf_env gl) ind).(0) in
    tclIFTHENELSE
      (tclTHENLIST
@@ -116,10 +116,10 @@ let left_and_tac ind backtrack id continue seq =
        tclDO n intro])
      (wrap n false continue seq)
      backtrack
-  end }
+  end
 
 let left_or_tac ind backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let v=construct_nhyps (pf_env gl) ind in
   let f n=
     tclTHENLIST
@@ -130,7 +130,7 @@ let left_or_tac ind backtrack id continue seq =
       (pf_constr_of_global id >>= simplest_elim)
       (Array.map f v)
       backtrack
-  end }
+  end
 
 let left_false_tac id=
   Tacticals.New.pf_constr_of_global id >>= simplest_elim
@@ -140,7 +140,7 @@ let left_false_tac id=
 (* We use this function for false, and, or, exists *)
 
 let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
      let rcs=ind_hyps (pf_env gl) (project gl) 0 indu largs in
      let vargs=Array.of_list largs in
              (* construire le terme  H->B, le generaliser etc *)
@@ -161,7 +161,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
 	       clear_global id;
 	       tclDO lp intro])
 	   (wrap lp false continue seq) backtrack
-  end }
+  end
 
 let ll_arrow_tac a b c backtrack id continue seq=
   let open EConstr in
@@ -199,7 +199,7 @@ let forall_tac backtrack continue seq=
        backtrack)
 
 let left_exists_tac ind backtrack id continue seq =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let n=(construct_nhyps (pf_env gl) ind).(0) in
     tclIFTHENELSE
       (Tacticals.New.pf_constr_of_global id >>= simplest_elim)
@@ -207,7 +207,7 @@ let left_exists_tac ind backtrack id continue seq =
                     tclDO n intro;
                     (wrap (n-1) false continue seq)])
       backtrack
-  end }
+  end
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
@@ -215,12 +215,12 @@ let ll_forall_tac prod backtrack id continue seq=
        [tclTHENLIST
 	  [intro;
            (pf_constr_of_global id >>= fun idc ->
-	   Proofview.Goal.enter { enter = begin fun gls->
+	   Proofview.Goal.enter begin fun gls->
               let open EConstr in
 	      let id0 = List.nth (pf_ids_of_hyps gls) 0 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
               tclTHEN (generalize [term]) (clear [id0])
-           end });
+           end);
 	   clear_global id;
 	   intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
@@ -239,9 +239,9 @@ let defined_connectives=lazy
    AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
 
 let normalize_evaluables=
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     unfold_in_concl (Lazy.force defined_connectives) <*>
     tclMAP
       (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
       (pf_ids_of_hyps gl)
-  end }
+  end
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a6290cb00c..317444cf16 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -469,7 +469,7 @@ exception GoalDone
 
 (* Résolution d'inéquations linéaires dans R *)
 let rec fourier () =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
@@ -633,7 +633,7 @@ let rec fourier () =
 (*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
       !tac
 (*      ((tclABSTRACT None !tac) gl) *)
-  end }
+  end
 ;;
 
 (*
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c2f705898f..fd49623986 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1481,7 +1481,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 			    tclCOMPLETE(
 				    Eauto.eauto_with_bases
 				      (true,5)
-				      [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+				      [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
 				      [Hints.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a0eb9e2b27..b8070ff885 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -12,7 +12,6 @@ open Context.Rel.Declaration
 open Indfun_common
 open Functional_principles_proofs
 open Misctypes
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
@@ -669,11 +668,9 @@ let build_case_scheme fa =
 	 let ind = first_fun_kn,funs_indexes in
 	   (ind,Univ.Instance.empty)(*FIXME*),prop_sort
   in
-  let sigma = Sigma.Unsafe.of_evar_map sigma in
-  let Sigma (scheme, sigma, _) = 
+  let (sigma, scheme) = 
       Indrec.build_case_analysis_scheme_default env sigma ind sf
   in
-  let sigma = Sigma.to_evar_map sigma in
   let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
   let sorts =
     (fun (_,_,x) ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index bd2ac8c67b..d28e0aba0a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -37,9 +37,10 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
     | Some b ->
-      let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
+      let (_, b) = b (Global.env ()) Evd.empty in
       spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
+
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a23c51495c..f1a9758e80 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -11,7 +11,6 @@ open Glob_term
 open Declarations
 open Misctypes
 open Decl_kinds
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
@@ -93,7 +92,7 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e6f199dbae..ff397d2e92 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -42,7 +42,6 @@ open Auto
 open Eauto
 
 open Indfun_common
-open Sigma.Notations
 open Context.Rel.Declaration
 
 (* Ugly things which should not be here *)
@@ -700,11 +699,9 @@ let mkDestructEq :
     observe_tclTHENLIST (str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
-        let changefun patvars = { run = fun sigma ->
-          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
-          let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) in
-          Sigma (c, sigma, p)
-        } in
+        let changefun patvars sigma =
+          pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
+        in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
@@ -1357,7 +1354,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 			  (Proofview.V82.of_tactic e_assumption);
 		      Eauto.eauto_with_bases
 			(true,5)
-			[{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+			[(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
 			[Hints.Hint_db.empty empty_transparent_state false]
 		      ]
 		    )
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 0a13a20a97..ea1660d901 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 bf84f61a5b..7db484d825 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 9726a5b401..8afe3053d0 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 50e8255a67..2c2a4b8509 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 23ce368eea..dd5307638c 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 5adf8475ae..25258ffa90 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 9029858279..9446f9df4d 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 f028abde9a..68dc1fd376 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 b78dc37426..cfb698cd87 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 37fdd185e9..ff76d06cf3 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 294cba4d75..e6d0370f36 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 *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 7497aae3ca..83f374346e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1668,8 +1668,6 @@ let rcst_domain_spec  = lazy {
  dump_proof = dump_psatz coq_Q dump_q
 }
 
-open Proofview.Notations
-
 (** Naive topological sort of constr according to the subterm-ordering *)
 
 (* An element is minimal x is minimal w.r.t y if 
@@ -1712,7 +1710,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
-  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+  Proofview.Goal.nf_enter begin fun gl -> 
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1724,7 +1722,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
       ]
       (Tacmach.New.pf_concl gl))
   ] 
-  end }
+  end
 
 
 (**
@@ -1972,7 +1970,7 @@ let micromega_gen
     (normalise:'cst atom -> 'cst mc_cnf)
     unsat deduce 
     spec dumpexpr prover tac =
- Proofview.Goal.nf_enter { enter = begin fun gl -> 
+ Proofview.Goal.nf_enter begin fun gl -> 
     let sigma = Tacmach.New.project gl in
     let concl = Tacmach.New.pf_concl gl in
     let hyps  = Tacmach.New.pf_hyps_types gl in
@@ -2029,7 +2027,7 @@ let micromega_gen
                             ^ "the use of a specialized external tool called csdp. \n\n" 
                             ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
                             ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-  end }
+  end
 
 let micromega_gen parse_arith 
     (negate:'cst atom -> 'cst mc_cnf)
@@ -2050,7 +2048,7 @@ let micromega_order_changer cert env ff  =
   let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
   let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
   let vm = dump_varmap (typ) (vm_of_list env) in
-  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+  Proofview.Goal.nf_enter begin fun gl -> 
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -2065,7 +2063,7 @@ let micromega_order_changer cert env ff  =
         (Tacmach.New.pf_concl gl)));
      (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
      ]
-  end }
+  end
 
 let micromega_genr prover tac =
   let parse_arith = parse_rarith in
@@ -2080,7 +2078,7 @@ let micromega_genr prover tac =
     proof_typ = Lazy.force coq_QWitness ;
     dump_proof = dump_psatz coq_Q dump_q
   } 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 = Tacmach.New.pf_concl gl in
      let hyps  = Tacmach.New.pf_hyps_types gl in
@@ -2144,7 +2142,7 @@ let micromega_genr prover tac =
                             ^ "the use of a specialized external tool called csdp. \n\n" 
                             ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
                             ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-  end }
+  end
 
 
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 0cd18ae506..465e770199 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -28,7 +28,6 @@ open Globnames
 open Nametab
 open Contradiction
 open Misctypes
-open Proofview.Notations
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -38,12 +37,12 @@ open OmegaSolver
 (* Added by JCF, 09/03/98 *)
 
 let elim_id id =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     simplest_elim (mkVar id)
-  end }
-let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
+  end
+let resolve_id id = Proofview.Goal.enter begin fun gl ->
   apply (mkVar id)
-end }
+end
 
 let timing timer_name f arg = f arg
 
@@ -580,10 +579,10 @@ let abstract_path sigma typ path t =
 
 let focused_simpl path =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
   convert_concl_no_check newc DEFAULTcast
-  end }
+  end
 
 let focused_simpl path = focused_simpl path
 
@@ -643,17 +642,16 @@ let decompile af =
 
 (** Backward compat to emulate the old Refine: normalize the goal conclusion *)
 let new_hole env sigma c =
-  let c = Reductionops.nf_betaiota (Sigma.to_evar_map sigma) c in
+  let c = Reductionops.nf_betaiota sigma c in
   Evarutil.new_evar env sigma c
 
 let clever_rewrite_base_poly typ p result theorem =
   let open Tacmach.New in
-  let open Sigma in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let full = pf_concl gl in
   let env = pf_env gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
-  Refine.refine { run = begin fun sigma ->
+  Refine.refine begin fun sigma ->
   let t =
     applist
       (mkLambda
@@ -667,10 +665,10 @@ let clever_rewrite_base_poly typ p result theorem =
        [abstracted])
   in
   let argt = mkApp (abstracted, [|result|]) in
-  let Sigma (hole, sigma, p) = new_hole env sigma argt in
-  Sigma (applist (t, [hole]), sigma, p)
-  end }
-  end }
+  let (sigma, hole) = new_hole env sigma argt in
+  (sigma, applist (t, [hole]))
+  end
+  end
 
 let clever_rewrite_base p result theorem =
   clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
@@ -689,26 +687,25 @@ let clever_rewrite_gen_nat p result (t,args) =
 (** Solve using the term the term [t _] *)
 let refine_app gl t =
   let open Tacmach.New in
-  let open Sigma in
-  Refine.refine { run = begin fun sigma ->
+  Refine.refine begin fun sigma ->
   let env = pf_env gl in
-  let ht = match EConstr.kind (Sigma.to_evar_map sigma) (pf_get_type_of gl t) with
+  let ht = match EConstr.kind sigma (pf_get_type_of gl t) with
   | Prod (_, t, _) -> t
   | _ -> assert false
   in
-  let Sigma (hole, sigma, p) = new_hole env sigma ht in
-  Sigma (applist (t, [hole]), sigma, p)
-  end }
+  let (sigma, hole) = new_hole env sigma ht in
+  (sigma, applist (t, [hole]))
+  end
 
 let clever_rewrite p vpath t =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
   let t' = applist(t, (vargs @ [abstracted])) in
   refine_app gl t'
-  end }
+  end
 
 let rec shuffle p (t1,t2) =
   match t1,t2 with
@@ -1466,7 +1463,7 @@ let reintroduce id =
 open Proofview.Notations
 
 let coq_omega =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   clear_constr_tables ();
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   let destructure_omega = destructure_omega gl in
@@ -1514,12 +1511,12 @@ let coq_omega =
       tclTHEN prelude (replay_history tactic_normalisation path)
     with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
   end
-  end }
+  end
 
 let coq_omega = coq_omega
 
 let nat_inject =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
   let rec explore p t : unit Proofview.tactic =
     Proofview.tclEVARMAP >>= fun sigma ->
@@ -1655,7 +1652,7 @@ let nat_inject =
   in
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   loop (List.rev hyps_types)
-  end }
+  end
 
 let dec_binop = function
   | Zne -> coq_dec_Zne
@@ -1729,19 +1726,19 @@ let onClearedName id tac =
   (* so renaming may be necessary *)
   tclTHEN
     (tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
+    (Proofview.Goal.nf_enter begin fun gl ->
      let id = fresh_id [] id gl in
      tclTHEN (introduction id) (tac id)
-    end })
+    end)
 
 let onClearedName2 id tac =
   tclTHEN
     (tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter { enter = begin fun gl ->
+    (Proofview.Goal.nf_enter begin fun gl ->
      let id1 = fresh_id [] (add_suffix id "_left") gl in
      let id2 = fresh_id [] (add_suffix id "_right") gl in
       tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
-    end })
+    end)
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
   | Sort s -> Sorts.is_prop (ESorts.kind sigma s)
@@ -1749,7 +1746,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
   | _ -> false
 
 let destructure_hyps =
-  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 decidability = decidability gl in
   let pf_nf = pf_nf gl in
@@ -1888,10 +1885,10 @@ let destructure_hyps =
     in
     let hyps = Proofview.Goal.hyps gl in
     loop hyps
-  end }
+  end
 
 let destructure_goal =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let decidability = decidability gl in
     let rec loop t =
@@ -1910,9 +1907,9 @@ let destructure_goal =
 	    try
 	      let dec = decidability t in
 	      tclTHEN
-                (Proofview.Goal.nf_enter { enter = begin fun gl ->
+                (Proofview.Goal.nf_enter begin fun gl ->
 		                         refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
-		                         end })
+		                         end)
 	        intro
 	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
 	    | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
@@ -1920,7 +1917,7 @@ let destructure_goal =
 	  tclTHEN goal_tac destructure_hyps
     in
     (loop concl)
-  end }
+  end
 
 let destructure_goal = destructure_goal
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 59ed8439b6..ffacd8b361 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -465,12 +465,12 @@ let pf_constrs_of_globals l =
   in aux l []
 
 let quote f lid =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let fg = Tacmach.New.pf_global f gl in
     let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
     Tacticals.New.pf_constr_of_global fg >>= fun f ->
     pf_constrs_of_globals clg >>= fun cl ->
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Tacmach.New.project gl in
       let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in
@@ -483,16 +483,16 @@ let quote f lid =
       match ivs.variable_lhs with
       | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
       | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
-    end }
-  end }
+    end
+  end
 
 let gen_quote cont c f lid =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let fg = Tacmach.New.pf_global f gl in
     let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
     Tacticals.New.pf_constr_of_global fg >>= fun f ->
     pf_constrs_of_globals clg >>= fun cl ->
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Tacmach.New.project gl in
       let cl = List.map (EConstr.to_constr sigma) cl in
@@ -505,8 +505,8 @@ let gen_quote cont c f lid =
       match ivs.variable_lhs with
       | None -> cont (mkApp (f, [| p |]))
       | Some _ -> cont (mkApp (f, [| vm; p |]))
-    end }
-  end }
+    end
+  end
 
 (*i
 
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index fbed1df176..d97dea0397 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -226,7 +226,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> Term.constr
   val parse_term : Term.constr -> parse_term
-  val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+  val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val get_scalar : Term.constr -> Bigint.bigint option
 end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index ca23ed6c42..a452b1a917 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -113,7 +113,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+    val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val get_scalar : Term.constr -> Bigint.bigint option
   end
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index fdcd622994..575634174f 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Util
-open Proofview.Notations
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1029,7 +1028,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
   Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
 let total_reflexive_omega_tactic unsafe =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
@@ -1043,4 +1042,5 @@ let total_reflexive_omega_tactic unsafe =
   if !debug then display_systems systems_list;
   resolution unsafe env reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
-  end }
+  end
+
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index cca5cde155..85cbdc5a41 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -749,7 +749,7 @@ let ltac_ring_structure e =
    lemma1;lemma2;pretac;posttac]
 
 let ring_lookup (f : Value.t) lH rl t =
-  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 (* find_ring_strucure can raise an exception *)
@@ -761,7 +761,7 @@ let ring_lookup (f : Value.t) lH rl t =
       let ring = ltac_ring_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end
 
 (***********************************************************************)
 
@@ -1035,7 +1035,7 @@ let ltac_field_structure e =
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
 let field_lookup (f : Value.t) lH rl t =
-  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
@@ -1047,4 +1047,4 @@ let field_lookup (f : Value.t) lH rl t =
       let field = ltac_field_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end
-- 
cgit v1.2.3