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.

13 files changed, 65 insertions, 116 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index efab5b977..c3f392980 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -32,7 +32,6 @@ open Evardefine
 open Evarsolve
 open Evarconv
 open Evd
-open Sigma.Notations
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -2000,10 +1999,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
         let sigma,t = match tycon with
 	| Some t -> refresh_tycon sigma t
 	| None -> 
-          let sigma = Sigma.Unsafe.of_evar_map sigma in
-          let Sigma ((t, _), sigma, _) =
+          let (sigma, (t, _)) =
 	    new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
-          let sigma = Sigma.to_evar_map sigma in
 	    sigma, t
 	in
         (* First strategy: we build an "inversion" predicate *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1d6b611da..3757ba7e6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -23,7 +23,6 @@ open Evardefine
 open Evarsolve
 open Evd
 open Pretype_errors
-open Sigma.Notations
 open Context.Named.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -913,9 +912,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	      (i,t2::ks, m-1, test)
 	  else
 	    let dloc = Loc.tag Evar_kinds.InternalHole in
-	    let i = Sigma.Unsafe.of_evar_map i in
-            let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
-            let i' = Sigma.to_evar_map i' in
+            let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
 	    (i', ev :: ks, m - 1,test))
 	(evd,[],List.length bs,fun i -> Success i) bs
     in
@@ -1099,9 +1096,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | None ->
         let evty = set_holes evdref cty subst in
         let instance = Filter.filter_list filter instance in
-        let evd = Sigma.Unsafe.of_evar_map !evdref in
-        let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
-        let evd = Sigma.to_evar_map evd in
+        let evd = !evdref in
+        let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
         evdref := evd;
         evsref := (fst (destEvar !evdref ev),evty)::!evsref;
         ev in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index a11619846..2d86daadb 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -17,15 +17,9 @@ open Namegen
 open Evd
 open Evarutil
 open Pretype_errors
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  (Sigma.to_evar_map evd, evk)
-
 let env_nf_evar sigma env =
   let nf_evar c = nf_evar sigma c in
   process_rel_context
@@ -82,9 +76,7 @@ let define_pure_evar_as_product evd evk =
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
-    let evd = Sigma.Unsafe.of_evar_map evd in
-    let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
-    (Sigma.to_evar_map evd1, e)
+    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi)
   in
   let evd2,rng =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
@@ -92,13 +84,11 @@ let define_pure_evar_as_product evd evk =
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
-        new_evar_unsafe newenv evd1 concl ~src ~filter
+        new_evar newenv evd1 concl ~src ~filter
       else
 	let status = univ_flexible_alg in
 	let evd3, (rng, srng) =
-          let evd1 = Sigma.Unsafe.of_evar_map evd1 in
-          let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
-          (Sigma.to_evar_map evd3, e)
+          new_type_evar newenv evd1 status ~src ~filter
         in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in
@@ -143,7 +133,7 @@ let define_pure_evar_as_lambda env evd evk =
   let newenv = push_named (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
-  let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de5a62726..ff0aeff75 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -20,7 +20,6 @@ open Retyping
 open Reductionops
 open Evarutil
 open Pretype_errors
-open Sigma.Notations
 
 let normalize_evar evd ev =
   match EConstr.kind evd (mkEvar ev) with
@@ -203,9 +202,7 @@ let restrict_evar_key evd evk filter candidates =
       let candidates = match candidates with
       | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
       | UpdateWith c -> Some c in
-      let sigma = Sigma.Unsafe.of_evar_map evd in
-      let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
-      (Sigma.to_evar_map sigma, evk)
+      restrict_evar evd evk filter candidates
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
@@ -649,9 +646,7 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
-  let evd = Sigma.to_evar_map evd in
+  let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
   let t_in_env = whd_evar evd t_in_env in
   let (evk, _) = destEvar evd evar_in_env in
   let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
@@ -721,10 +716,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
      ~status:univ_flexible (Some false) env evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (ev2_in_sign, evd, _) =
+  let (evd, ev2_in_sign) =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
-  let evd = Sigma.to_evar_map evd in
   let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8a902f3a3..97aec1814 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -27,7 +27,6 @@ open Inductiveops
 open Environ
 open Reductionops
 open Nametab
-open Sigma.Notations
 open Context.Rel.Declaration
 
 type dep_flag = bool
@@ -130,19 +129,19 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 	it_mkLambda_or_LetIn_name env' obj deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
-      let t = build_branch_type env (Sigma.to_evar_map sigma) dep (mkRel (k+1)) cs in
+      let t = build_branch_type env sigma dep (mkRel (k+1)) cs in
       mkLambda_string "f" t
 	(add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1))
   in
-  let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
-  let typP = make_arity env' (Sigma.to_evar_map sigma) dep indf s in
+  let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
+  let typP = make_arity env' sigma dep indf s in
   let typP = EConstr.Unsafe.to_constr typP in
   let c = 
     it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
      (add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar
   in
-  Sigma (c, sigma, p)
+  (sigma, c)
 
 (* check if the type depends recursively on one of the inductive scheme *)
 
@@ -475,10 +474,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
 	    lnamesparrec
       else
-        let sigma = Sigma.Unsafe.of_evar_map !evdref in
-        let Sigma (c, sigma, _) = mis_make_case_com dep env sigma (indi,u) (mibi,mipi) kind in
-        let evd' = Sigma.to_evar_map sigma in
-	  evdref := evd'; c
+        let evd = !evdref in
+        let (evd, c) = mis_make_case_com dep env evd (indi,u) (mibi,mipi) kind in
+	  evdref := evd; c
   in
     (* Body of mis_make_indrec *)
     !evdref, List.init nrec make_one_rec
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 192b64a5e..a22470ae8 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -26,14 +26,14 @@ type dep_flag = bool
 
 (** Build a case analysis elimination scheme in some sort family *)
 
-val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
-      dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
+val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive ->
+      dep_flag -> sorts_family -> evar_map * Constr.t
 
 (** Build a dependent case elimination predicate unless type is in Prop
    or is a recursive record with primitive projections. *)
 
-val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
-      sorts_family -> (constr, 'r) Sigma.sigma
+val build_case_analysis_scheme_default : env -> evar_map -> pinductive ->
+      sorts_family -> evar_map * Constr.t
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
    sort family as the inductive family; it is dependent if not in Prop
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 08a6dd4db..92e728683 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,8 +44,6 @@ open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
-open Tactypes
-open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
 
@@ -111,9 +109,9 @@ let e_new_evar env evdref ?src ?naming typ =
   let typ' = subst2 subst vsubst typ in
   let instance = inst_rels @ inst_vars in
   let sign = val_of_named_context nc in
-  let sigma = Sigma.Unsafe.of_evar_map !evdref in
-  let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in
-  evdref := Sigma.to_evar_map sigma;
+  let sigma = !evdref in
+  let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in
+  evdref := sigma;
   e
 
 let push_rec_types sigma (lna,typarray,_) env =
@@ -390,9 +388,8 @@ let adjust_evar_source evdref na c =
      begin match evi.evar_source with
      | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
         let src = (loc,Evar_kinds.QuestionMark (b,na)) in
-        let sigma = Sigma.Unsafe.of_evar_map !evdref in
-        let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
-        evdref := Sigma.to_evar_map evd;
+        let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in
+        evdref := evd;
         mkEvar (evk',args)
      | _ -> c
      end
@@ -571,12 +568,12 @@ let pretype_sort ?loc evdref = function
   | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s
 
 let new_type_evar env evdref loc =
-  let sigma = Sigma.Unsafe.of_evar_map !evdref in
-  let Sigma ((e, _), sigma, _) =
+  let sigma = !evdref in
+  let (sigma, (e, _)) =
     Evarutil.new_type_evar env.ExtraEnv.env sigma
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
   in
-  evdref := Sigma.to_evar_map sigma;
+  evdref := sigma;
   e
 
 module ConstrInterpObj =
@@ -1267,7 +1264,7 @@ let constr_flags = {
 (* Fully evaluate an untyped constr *)
 let type_uconstr ?(flags = constr_flags)
   ?(expected_type = WithoutTypeConstraint) ist c =
-  { delayed = begin fun env sigma ->
+  begin fun env sigma ->
   let { closure; term } = c in
   let vars = {
     ltac_constrs = closure.typed;
@@ -1275,10 +1272,8 @@ let type_uconstr ?(flags = constr_flags)
     ltac_idents = closure.idents;
     ltac_genargs = Id.Map.empty;
   } in
-  let sigma = Sigma.to_evar_map sigma in
-  let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
-  Sigma.Unsafe.of_pair (c, sigma)
-  end }
+  understand_ltac flags env sigma vars expected_type term
+  end
 
 let pretype k0 resolve_tc typcon env evdref lvar t =
   pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 2fa3facb3..f9be82024 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -41,13 +41,8 @@ let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
 let coq_not = init_reference ["Init";"Logic"] "not"
 let coq_and = init_reference ["Init";"Logic"] "and"
 
-let new_global sigma gr =
-  let open Sigma in
-  let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
-  in Sigma.to_evar_map sigma, c
-
 let mk_coq_not sigma x =
-  let sigma, notc = new_global sigma (coq_not ()) in
+  let sigma, notc = Evarutil.new_global sigma (coq_not ()) in
   sigma, EConstr.mkApp (notc, [| x |])
 
 let unsafe_fold_right f = function
@@ -55,7 +50,7 @@ let unsafe_fold_right f = function
   | [] -> invalid_arg "unsafe_fold_right"
 
 let mk_coq_and sigma l =
-  let sigma, and_typ = new_global sigma (coq_and ()) in
+  let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in
   sigma, unsafe_fold_right
       (fun c conj ->
 	 EConstr.mkApp (and_typ, [| c ; conj |]))
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c976fe66d..b4654bfb5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -595,7 +595,7 @@ type state = constr * constr Stack.t
 type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
 type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
 type contextual_stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index af8048156..af0e28cdd 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -117,7 +117,7 @@ type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
 type local_reduction_function = evar_map -> constr -> constr
 
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
 type contextual_stack_reduction_function =
     env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f2b0995b0..ec3669bfe 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -24,7 +24,6 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
-open Sigma.Notations
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
@@ -399,9 +398,8 @@ let substl_with_function subst sigma constr =
     if i <= k + Array.length v then
       match v.(i-k-1) with
       | (fx, Some (min, ref)) ->
-        let sigma = Sigma.Unsafe.of_evar_map !evd in
-        let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in
-        let sigma = Sigma.to_evar_map sigma in
+        let sigma = !evd in
+        let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in
         evd := sigma;
         minargs := Evar.Map.add evk min !minargs;
         Vars.lift k (mkEvar (evk, [|fx;ref|]))
@@ -983,11 +981,10 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
       | _ -> mkApp (app', [| a' |]))
   | _ -> map_constr_with_binders_left_to_right sigma g f acc c
 
-let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
+let e_contextually byhead (occs,c) f = begin fun env sigma t ->
   let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
-  let sigma = Sigma.to_evar_map sigma in
   (** FIXME: we do suspicious things with this evarmap *)
   let evd = ref sigma in
   let rec traverse nested (env,c as envc) t =
@@ -1007,8 +1004,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
         (* Skip inner occurrences for stable counting of occurrences *)
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
-	let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in
-	(evd := Sigma.to_evar_map evm; t)
+	let (evm, t) = (f subst) env !evd t in
+	(evd := evm; t)
       end
       else
 	traverse_below nested envc t
@@ -1027,15 +1024,12 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
   in
   let t' = traverse None (env,c) t in
   if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
-  Sigma.Unsafe.of_pair (t', !evd)
-  end }
+  (!evd, t')
+  end
 
 let contextually byhead occs f env sigma t =
-  let f' subst = { e_redfun = begin fun env sigma t ->
-    Sigma.here (f subst env (Sigma.to_evar_map sigma) t) sigma
-  end } in
-  let Sigma (c, _, _) = (e_contextually byhead occs f').e_redfun env (Sigma.Unsafe.of_evar_map sigma) t in
-  c
+  let f' subst env sigma t = sigma, f subst env sigma t in
+  snd (e_contextually byhead occs f' env sigma t)
 
 (* linear bindings (following pretty-printer) of the value of name in c.
  * n is the number of the next occurrence of name.
@@ -1154,15 +1148,14 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
     let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
       mkLambda (na,ta,c'), sigma'
 
-let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
-  let sigma = Sigma.to_evar_map sigma in
+let pattern_occs loccs_trm = begin fun env sigma c ->
   let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
   try
     let _ = Typing.unsafe_type_of env sigma abstr_trm in
-    Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
+    (sigma, applist(abstr_trm, List.map snd loccs_trm))
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
-  end }
+  end
 
 (* Used in several tactics. *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d1643a8c7..0fb48ed8c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -31,7 +31,6 @@ open Recordops
 open Locus
 open Locusops
 open Find_subterm
-open Sigma.Notations
 
 type metabinding = (metavariable * EConstr.constr * (instance_constraint * instance_typing_status))
 
@@ -145,9 +144,7 @@ let set_occurrences_of_last_arg args =
   Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
 
 let abstract_list_all_with_dependencies env evd typ c l =
-  let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (ev, evd, _) = new_evar env evd typ in
-  let evd = Sigma.to_evar_map evd in
+  let (evd, ev) = new_evar env evd typ in
   let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in
   let n = List.length l in
   let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
@@ -1239,20 +1236,19 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
  * close it off.  But this might not always work,
  * since other metavars might also need to be resolved. *)
 
-let applyHead env (type r) (evd : r Sigma.t) n c =
-  let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma =
-    fun n c cty p evd ->
+let applyHead env evd n c  =
+  let rec apprec n c cty evd =
     if Int.equal n 0 then
-      Sigma (c, evd, p)
+      (evd, c)
     else
-      let sigma = Sigma.to_evar_map evd in
-      match EConstr.kind sigma (whd_all env sigma cty) with
+      match EConstr.kind evd (whd_all env evd cty) with
       | Prod (_,c1,c2) ->
-        let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
-	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
+        let (evd',evar) =
+      Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
+      apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
       | _ -> user_err Pp.(str "Apply_Head_Then")
   in
-    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
+    apprec n c (Typing.unsafe_type_of env evd c) evd
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with
@@ -1416,9 +1412,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
   and mimick_undefined_evar evd flags hdc nargs sp =
     let ev = Evd.find_undefined evd sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
-    let evd = Sigma.Unsafe.of_evar_map evd in
-    let Sigma (c, evd', _) = applyHead sp_env evd nargs hdc in
-    let evd' = Sigma.to_evar_map evd' in
+    let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' CUMUL flags
         (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in
@@ -1534,10 +1528,9 @@ let indirectly_dependent sigma c d decls =
     List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
-  let current_sigma = Sigma.to_evar_map current_sigma in
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
   let sigma, subst = nf_univ_variables sigma in
-  Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))), sigma)
+  (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
 
 let default_matching_core_flags sigma =
   let ts = Names.full_transparent_state in {
@@ -1684,7 +1677,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
     let res = match out test with
     | None -> None
-    | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma))
+    | Some (sigma, c) -> Some (sigma,c)
     in
     (id,sign,depdecls,lastlhyp,ccl,res)
   with
@@ -1711,10 +1704,9 @@ type abstraction_request =
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
     named_declaration list * Names.Id.t option *
-    types * (constr, 'r) Sigma.sigma option
+    types * (evar_map * constr) option
 
 let make_abstraction env evd ccl abs =
-  let evd = Sigma.to_evar_map evd in
   match abs with
   | AbstractPattern (from_prefix,check,name,c,occs,check_occs) ->
       make_abstraction_core name
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8d7e3521d..0d90ab158 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -76,14 +76,14 @@ type abstraction_request =
 | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
 
 val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
-  env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma
+  env -> evar_map -> (evar_map * constr) -> evar_map * constr
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
     named_declaration list * Names.Id.t option *
-    types * (constr, 'r) Sigma.sigma option
+    types * (evar_map * constr) option
 
-val make_abstraction : env -> 'r Sigma.t -> constr ->
+val make_abstraction : env -> evar_map -> constr ->
   abstraction_request -> 'r abstraction_result
 
 val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr