Monotonizing the Evarutil module.

Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.

14 files changed, 136 insertions, 64 deletions

diff --git a/engine/sigma.ml b/engine/sigma.ml
index e886b0d1e7..c25aac0c14 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,6 +36,18 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
+let new_univ_level_variable ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let new_univ_variable ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
+let new_sort_variable ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in
+  Sigma (u, sigma, ())
+
 let fresh_sort_in_family ?rigid env sigma s =
   let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
   Sigma (s, sigma, ())
diff --git a/engine/sigma.mli b/engine/sigma.mli
index cb948dba59..d7ae2e4ac9 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -66,6 +66,13 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
+val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+  'r t -> (Univ.universe_level, 'r) sigma
+val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+  'r t -> (Univ.universe, 'r) sigma
+val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+  'r t -> (Sorts.t, 'r) sigma
+
 val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
   'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
 val fresh_constant_instance :
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a717cc91ea..fcbad46d46 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,6 +22,7 @@ open Formula
 open Sequent
 open Names
 open Misctypes
+open Sigma.Notations
 
 let compare_instance inst1 inst2=
 	match inst1,inst2 with
@@ -116,7 +117,9 @@ let mk_open_instance id idc gl m t=
   let rec aux n avoid env evmap decls =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id avoid var_id gl) in
-      let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible 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 decl = (Name nid,None,c) in
 	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2cbf3a2650..91bf11eb52 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -28,6 +28,7 @@ open Evarutil
 open Evarsolve
 open Evarconv
 open Evd
+open Sigma.Notations
 
 (* Pattern-matching errors *)
 
@@ -1947,8 +1948,10 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
         let sigma,t = match tycon with
 	| Some t -> sigma,t
 	| None -> 
-	  let sigma, (t, _) = 
+          let sigma = Sigma.Unsafe.of_evar_map sigma in
+          let Sigma ((t, _), sigma, _) =
 	    new_type_evar env sigma univ_flexible_alg ~src:(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 99e51330ef..f3ff26876c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1007,7 +1007,9 @@ 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,ev = new_evar_instance sign !evdref evty ~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
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
         ev in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 0dd0ad2e08..518f4df408 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -19,6 +19,7 @@ open Retyping
 open Reductionops
 open Evarutil
 open Pretype_errors
+open Sigma.Notations
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -180,7 +181,9 @@ let restrict_evar_key evd evk filter candidates =
       let candidates = match candidates with
       | NoUpdate -> evi.evar_candidates
       | UpdateWith c -> Some c in
-      restrict_evar evd evk filter candidates
+      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)
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
@@ -570,7 +573,9 @@ 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,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  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 t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -631,8 +636,10 @@ 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,ev2_in_sign =
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (ev2_in_sign, evd, _) =
     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 ev2_in_sign), Array.of_list inst2_in_env) in
   (evd, ev2_in_sign, ev2_in_env)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cd5188cd75..2ed557683e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -19,6 +19,7 @@ open Environ
 open Evd
 open Reductionops
 open Pretype_errors
+open Sigma.Notations
 
 (** Combinators *)
 
@@ -41,7 +42,7 @@ let e_new_global evdref x =
   evd_comb1 (Evd.fresh_global (Global.env())) evdref x
 
 let new_global evd x = 
-  Evd.fresh_global (Global.env()) evd x
+  Sigma.fresh_global (Global.env()) evd x
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
@@ -342,15 +343,18 @@ let push_rel_context_to_named_context env typ =
 let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
 let restrict_evar evd evk filter candidates =
+  let evd = Sigma.to_evar_map evd in
   let evd, evk' = Evd.restrict evk filter ?candidates evd in
-  Evd.declare_future_goal evk' evd, evk'
+  Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
 
 let new_pure_evar_full evd evi =
+  let evd = Sigma.to_evar_map evd in
   let (evd, evk) = Evd.new_evar evd evi in
   let evd = Evd.declare_future_goal evk evd in
-  (evd, evk)
+  Sigma.Unsafe.of_pair (evk, evd)
 
 let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
+  let evd = Sigma.to_evar_map evd in
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let evi = {
@@ -367,17 +371,17 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
   in
-  (evd,newevk)
+  Sigma.Unsafe.of_pair (newevk, evd)
 
 let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  (evd,mkEvar (newevk,Array.of_list instance))
+  let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
   let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
@@ -386,24 +390,26 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-  let evd = Sigma.to_evar_map evd in
-  let (sigma, c) = new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
-  Sigma.Unsafe.of_pair (c, sigma)
+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 new_type_evar env evd ?src ?filter ?naming ?principal rigid =
-  let evd', s = new_sort_variable rigid evd in
-  let evd', e = new_evar_unsafe env evd' ?src ?filter ?naming ?principal (mkSort s) in
-    evd', (e, s)
+  let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
+  let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+  Sigma ((e, s), evd', p +> q)
 
 let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
-  let evd', c = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
-    evdref := evd';
+  let sigma = Sigma.Unsafe.of_evar_map !evdref in
+  let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
+  let sigma = Sigma.to_evar_map sigma in
+    evdref := sigma;
     c
 
 let new_Type ?(rigid=Evd.univ_flexible) env evd = 
-  let evd', s = new_sort_variable rigid evd in
-    evd', mkSort s
+  let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
+  Sigma (mkSort s, sigma, p)
 
 let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
   let evd', s = new_sort_variable rigid !evdref in
@@ -501,7 +507,9 @@ let rec check_and_clear_in_constr env evdref err ids c =
             else
               let origfilter = Evd.evar_filter evi in
               let filter = Evd.Filter.apply_subfilter origfilter filter in
-              let evd,_ = restrict_evar !evdref evk filter None in
+              let evd = Sigma.Unsafe.of_evar_map !evdref in
+              let Sigma (_, evd, _) = restrict_evar evd evk filter None in
+              let evd = Sigma.to_evar_map evd in
               evdref := evd;
 	    (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
 	      let evi = Evd.find !evdref evk in
@@ -708,7 +716,10 @@ let define_pure_evar_as_product evd evk =
   let concl = whd_betadeltaiota evenv evd evi.evar_concl in
   let s = destSort concl in
   let evd1,(dom,u1) =
-    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+    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)
+  in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
@@ -719,7 +730,10 @@ let define_pure_evar_as_product evd evk =
       else
 	let status = univ_flexible_alg in
 	let evd3, (rng, srng) =
-	  new_type_evar newenv evd1 status ~src ~filter in
+          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)
+        in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
 	  evd3, rng
@@ -798,8 +812,8 @@ let define_evar_as_sort env evd (ev,args) =
    any type has type Type. May cause some trouble, but not so far... *)
 
 let judge_of_new_Type evd =
-  let evd', s = new_univ_variable univ_rigid evd in
-    evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
+  let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
+  Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
 
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d87c7ef8d1..bc4c37a918 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -27,12 +27,12 @@ val new_evar :
   ?principal:bool -> types -> (constr, 'r) Sigma.sigma
 
 val new_pure_evar :
-  named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * evar
+  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
 
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
+val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
 
 (** the same with side-effects *)
 val e_new_evar :
@@ -44,23 +44,23 @@ val e_new_evar :
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
-  env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  evar_map * (constr * sorts)
+  (constr * sorts, 'r) Sigma.sigma
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
-val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
+val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
-val restrict_evar : evar_map -> existential_key -> Filter.t ->
-  constr list option -> evar_map * existential_key
+val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
+  constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
-val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
+val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
 val e_new_global : evar_map ref -> Globnames.global_reference -> constr
 
 (** Create a fresh evar in a context different from its definition context:
@@ -70,11 +70,11 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> 
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> 
+ named_context_val -> 'r Sigma.t -> types -> 
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
-  constr list -> evar_map * constr
+  constr list -> (constr, 'r) Sigma.sigma
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
@@ -138,7 +138,7 @@ val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
 
 (** {6 Value/Type constraints} *)
 
-val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
+val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 
 type type_constraint = types option
 type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11fba7b941..835dc2f808 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,6 +42,7 @@ open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
+open Sigma.Notations
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = constr_under_binders Id.Map.t
@@ -444,10 +445,13 @@ let pretype_sort evdref = function
   | GType s -> evd_comb1 judge_of_Type evdref s
 
 let new_type_evar env evdref loc =
-  let e, s = 
-    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
-      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
-  in e
+  let sigma = Sigma.Unsafe.of_evar_map !evdref in
+  let Sigma ((e, _), sigma, _) =
+    Evarutil.new_type_evar env sigma
+      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
+  in
+  evdref := Sigma.to_evar_map sigma;
+  e
 
 let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bd46911c92..085aaf78a1 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,6 +23,7 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
+open Sigma.Notations
 
 (* Errors *)
 
@@ -385,7 +386,9 @@ 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, evk) = Evarutil.new_pure_evar venv !evd dummy in
+        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
         evd := sigma;
         minargs := Evar.Map.add evk min !minargs;
         lift k (mkEvar (evk, [|fx;ref|]))
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 43a3024e50..1251dacd5d 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,6 +9,7 @@
 open Util
 open Pp
 open Term
+open Sigma.Notations
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -70,7 +71,9 @@ module V82 = struct
 		Evd.evar_extra = extra }
     in
     let evi = Typeclasses.mark_unresolvable evi in
-    let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
+    let evars = Sigma.Unsafe.of_evar_map evars in
+    let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in
+    let evars = Sigma.to_evar_map evars in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
@@ -126,8 +129,10 @@ module V82 = struct
     let new_evi =
       { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in
-    let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
-    { Evd.it = evk ; sigma = new_sigma; }
+    let sigma = Sigma.Unsafe.of_evar_map Evd.empty in
+    let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in
+    let sigma = Sigma.to_evar_map sigma in
+    { Evd.it = evk ; sigma = sigma; }
 
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 29002af9e0..c50535a17a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -64,8 +64,10 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
 let find_global dir s =
   let gr = lazy (try_find_global_reference dir s) in
-    fun (evd,cstrs) -> 
-      let evd, c = Evarutil.new_global evd (Lazy.force gr) 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
 	(evd, cstrs), c
 
 (** Utility for dealing with polymorphic applications *)
@@ -172,13 +174,17 @@ end) = struct
   let proper_type = 
     let l = lazy (Lazy.force proper_class).cl_impl in
       fun (evd,cstrs) -> 
-	let evd, c = Evarutil.new_global evd (Lazy.force l) in
+        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
 	  (evd, cstrs), c
 	
   let proper_proxy_type = 
     let l = lazy (Lazy.force proper_proxy_class).cl_impl in
       fun (evd,cstrs) -> 
-	let evd, c = Evarutil.new_global evd (Lazy.force l) in
+        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
 	  (evd, cstrs), c
 
   let proper_proof env evars carrier relation x =
@@ -347,7 +353,9 @@ end) = struct
 	  (try
 	   let params, args = Array.chop (Array.length args - 2) args in
 	   let env' = Environ.push_rel_context rels env in
-	   let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible 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 sigma in
 	   let evars, inst = 
 	     app_poly env (evars,Evar.Set.empty)
 	       rewrite_relation_class [| evar; mkApp (c, params) |] in
@@ -407,7 +415,9 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+    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
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aeb3726a0c..46e8798543 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,14 +163,13 @@ let _ =
     does not check anything. *)
 let unsafe_intro env store (id, c, t) b =
   Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-    let sigma = Sigma.to_evar_map sigma in
     let ctx = named_context_val env in
     let nctx = push_named_context_val (id, c, t) ctx in
     let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar id) b in
-    let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
-    Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
+    let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+    Sigma (mkNamedLambda_or_LetIn (id, c, t) ev, sigma, p)
   end }
 
 let introduction ?(check=true) id =
@@ -344,9 +343,7 @@ let rename_hyp repl =
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
       Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-        let sigma = Sigma.to_evar_map sigma in
-        let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
-        Sigma.Unsafe.of_pair (c, sigma)
+        Evarutil.new_evar_instance nctx sigma nconcl ~store instance
       end }
     end }
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 7ae2030343..480e97169c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -24,6 +24,7 @@ open Type_errors
 open Constrexpr
 open Constrexpr_ops
 open Goptions
+open Sigma.Notations
 
 (********** definition d'un record (structure) **************)
 
@@ -336,11 +337,15 @@ let structure_signature ctx =
     match l with [] -> Evd.empty
       | [(_,_,typ)] ->
         let env = Environ.empty_named_context_val in
-        let (evm, _) = Evarutil.new_pure_evar env evm typ in
+        let evm = Sigma.Unsafe.of_evar_map evm in
+        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm typ in
+        let evm = Sigma.to_evar_map evm in
         evm
       | (_,_,typ)::tl ->
           let env = Environ.empty_named_context_val in
-          let (evm, ev) = Evarutil.new_pure_evar env evm typ in
+          let evm = Sigma.Unsafe.of_evar_map evm in
+          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm typ in
+          let evm = Sigma.to_evar_map evm in
 	  let new_tl = Util.List.map_i
 	    (fun pos (n,c,t) -> n,c,
 	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in