Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.

18 files changed, 453 insertions, 379 deletions

diff --git a/API/API.mli b/API/API.mli
index 8f46a5832..6326247f8 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4620,6 +4620,9 @@ end
 
 module Constrintern :
 sig
+
+  open Evd
+
   type ltac_sign = {
     ltac_vars : Names.Id.Set.t;
     ltac_bound : Names.Id.Set.t;
@@ -4635,11 +4638,11 @@ sig
     | Variable
   type internalization_env = var_internalization_data Names.Id.Map.t
 
-  val interp_constr_evars : Environ.env -> Evd.evar_map ref ->
-                            ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr
+  val interp_constr_evars : Environ.env -> evar_map ->
+                            ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr
 
-  val interp_type_evars : Environ.env -> Evd.evar_map ref ->
-                          ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types
+  val interp_type_evars : Environ.env -> Evd.evar_map ->
+                          ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types
 
   val empty_ltac_sign : ltac_sign
   val intern_gen : Pretyping.typing_constraint -> Environ.env ->
@@ -4657,10 +4660,12 @@ sig
   val locate_reference :  Libnames.qualid -> Globnames.global_reference
   val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env ->
                     Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context
+
   val interp_context_evars :
     ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
-    Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list ->
-    internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)
+    Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list ->
+    evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))
+
   val compute_internalization_data : Environ.env -> var_internalization_type ->
                                      Constr.types -> Impargs.manual_explicitation list -> var_internalization_data
   val empty_internalization_env : internalization_env
diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
new file mode 100644
index 000000000..8aea7dee3
--- /dev/null
+++ b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then
+    Equations_CI_BRANCH=interp+less_impstyle_p2
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index c69be4f4d..01aa6b599 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -46,6 +46,11 @@ We changed the type of the following functions:
 
 - `Global.body_of_constant`: same as above.
 
+- `Constrinterp.*` generally, many functions that used to take an
+  `evar_map ref` have been now switched to functions that will work in
+  a functional way. The old style of passing `evar_map`s as references
+  is not supported anymore.
+
 We have changed the representation of the following types:
 
 - `Lib.object_prefix` is now a record instead of a nested tuple.
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 53123c933..a65b3941e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -770,6 +770,20 @@ let rec isArity sigma c =
   | Sort _          -> true
   | _               -> false
 
+type arity = rel_context * ESorts.t
+
+let destArity sigma =
+  let open Context.Rel.Declaration in
+  let rec prodec_rec l c =
+    match kind sigma c with
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
+    | Cast (c,_,_)      -> prodec_rec l c
+    | Sort s          -> l,s
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity.")
+  in
+  prodec_rec []
+
 let mkProd_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
@@ -817,6 +831,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
 let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
 
+let map_rel_context_in_env f env sign =
+  let rec aux env acc = function
+    | d::sign ->
+        aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign
+    | [] ->
+        acc
+  in
+  aux env [] (List.rev sign)
+
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, of_constr t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 6f2a30f4a..30de748a1 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -146,7 +146,11 @@ val isFix : Evd.evar_map -> t -> bool
 val isCoFix : Evd.evar_map -> t -> bool
 val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
+
+type arity = rel_context * ESorts.t
+val destArity : Evd.evar_map -> types -> arity
 val isArity : Evd.evar_map -> t -> bool
+
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
 val isRelN : Evd.evar_map -> int -> t -> bool
 
@@ -262,6 +266,9 @@ val lookup_rel : int -> env -> rel_declaration
 val lookup_named : variable -> env -> named_declaration
 val lookup_named_val : variable -> named_context_val -> named_declaration
 
+val map_rel_context_in_env :
+  (env -> constr -> constr) -> env -> rel_context -> rel_context
+
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 14234b311..61b33aa41 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2098,39 +2098,36 @@ let interp_open_constr env sigma c =
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_constr_evars_gen_impls env evdref
+let interp_constr_evars_gen_impls env sigma
     ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-  let evd, c = understand_tcc env !evdref ~expected_type c in
-  evdref := evd;
-  c, imps
+  let sigma, c = understand_tcc env sigma ~expected_type c in
+  sigma, (c, imps)
 
-let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c
 
 let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
   interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
 
-let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env evdref ~impls IsType c
+let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls env sigma ~impls IsType c
 
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
-let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env c in
-  let evd, c = understand_tcc env !evdref ~expected_type c in
-  evdref := evd;
-  c
+  understand_tcc env sigma ~expected_type c
 
 let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
 
-let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen env sigma ~impls (OfType typ) c
 
-let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen env evdref IsType ~impls c
+let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen env sigma IsType ~impls c
 
 (* Miscellaneous *)
 
@@ -2185,17 +2182,16 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
-let interp_glob_context_evars env evdref k bl =
+let interp_glob_context_evars env sigma k bl =
   let open EConstr in
-  let (env, par, _, impls) =
+  let env, sigma, par, _, impls =
     List.fold_left
-      (fun (env,params,n,impls) (na, k, b, t) ->
+      (fun (env,sigma,params,n,impls) (na, k, b, t) ->
        let t' =
 	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
-       let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in
-       evdref := evd;
+       let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in
 	match b with
 	    None ->
 	      let d = LocalAssum (na,t) in
@@ -2205,16 +2201,15 @@ let interp_glob_context_evars env evdref k bl =
 		    (ExplByPos (n, na), (true, true, true)) :: impls
 		else impls
 	      in
-		(push_rel d env, d::params, succ n, impls)
+                (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
-	      let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in
-              evdref := evd;
+              let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in
 	      let d = LocalDef (na, c, t) in
-		(push_rel d env, d::params, n, impls))
-      (env,[],k+1,[]) (List.rev bl)
-  in (env, par), impls
+                (push_rel d env, sigma, d::params, n, impls))
+      (env,sigma,[],k+1,[]) (List.rev bl)
+  in sigma, ((env, par), impls)
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_glob_context_evars env evdref shift bl in
-  int_env, x
+  let sigma, x = interp_glob_context_evars env sigma shift bl in
+  sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index af4e4a9c5..632b423b0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -112,29 +112,28 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.co
 
 (** Accepting unresolved evars *)
 
-val interp_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> EConstr.constr
+val interp_constr_evars : env -> evar_map ->
+  ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr
 
+val interp_casted_constr_evars : env -> evar_map ->
+  ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr
 
-val interp_casted_constr_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> EConstr.types -> EConstr.constr
-
-val interp_type_evars : env -> evar_map ref ->
-  ?impls:internalization_env -> constr_expr -> EConstr.types
+val interp_type_evars : env -> evar_map ->
+  ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_constr_evars_impls : env -> evar_map ref ->
+val interp_constr_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
-  EConstr.constr * Impargs.manual_implicits
+  evar_map * (EConstr.constr * Impargs.manual_implicits)
 
-val interp_casted_constr_evars_impls : env -> evar_map ref ->
+val interp_casted_constr_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> EConstr.types ->
-  EConstr.constr * Impargs.manual_implicits
+  evar_map * (EConstr.constr * Impargs.manual_implicits)
 
-val interp_type_evars_impls : env -> evar_map ref ->
+val interp_type_evars_impls : env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
-  EConstr.types * Impargs.manual_implicits
+  evar_map * (EConstr.types * Impargs.manual_implicits)
 
 (** Interprets constr patterns *)
 
@@ -159,8 +158,8 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
-  env -> evar_map ref -> local_binder_expr list ->
-  internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)
+  env -> evar_map -> local_binder_expr list ->
+  evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits))
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
diff --git a/lib/cList.ml b/lib/cList.ml
index ca69628af..0ef7c3d8b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -96,6 +96,8 @@ sig
   val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
   val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
   val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
+  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
@@ -446,6 +448,12 @@ let rec fold_left3 f accu l1 l2 l3 =
   | (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
   | (_, _, _) -> invalid_arg "List.fold_left3"
 
+let rec fold_left4 f accu l1 l2 l3 l4 =
+  match (l1, l2, l3, l4) with
+    ([], [], [], []) -> accu
+  | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4
+  | (_,_, _, _) -> invalid_arg "List.fold_left4"
+
 (* [fold_right_and_left f [a1;...;an] hd =
    f (f (... (f (f hd
                    an
@@ -765,12 +773,13 @@ let share_tails l1 l2 =
   in
   shr_rev [] (List.rev l1, List.rev l2)
 
+(* Poor man's monadic map *)
 let rec fold_left_map f e = function
-  |  []  -> (e,[])
-  |  h::t ->
-       let e',h' = f e h in
-       let e'',t' = fold_left_map f e' t in
-         e'',h'::t'
+  | []  -> (e,[])
+  | h::t ->
+    let e',h' = f e h in
+    let e'',t' = fold_left_map f e' t in
+    e'',h'::t'
 
 let fold_map = fold_left_map
 
@@ -790,12 +799,26 @@ let fold_right_map f l e =
 
 let fold_map' = fold_right_map
 
+let on_snd f (x,y) = (x,f y)
+
 let fold_left2_map f e l l' =
-  List.fold_left2 (fun (e,l) x x' -> let (e,y) = f e x x' in (e,y::l)) (e,[]) l l'
+  on_snd List.rev @@
+  List.fold_left2 (fun (e,l) x x' ->
+      let (e,y) = f e x x' in
+      (e, y::l)
+    ) (e, []) l l'
 
 let fold_right2_map f l l' e =
   List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e)
 
+let fold_left3_map f e l l' l'' =
+  on_snd List.rev @@
+  fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l''
+
+let fold_left4_map f e l1 l2 l3 l4 =
+  on_snd List.rev @@
+  fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4
+
 let map_assoc f = List.map (fun (x,a) -> (x,f a))
 
 let rec assoc_f f a = function
diff --git a/lib/cList.mli b/lib/cList.mli
index 8cb07da79..f87db04cf 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -211,7 +211,14 @@ sig
   val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
   (** Same with two lists, folding on the right *)
 
+  val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+  (** Same with three lists, folding on the left *)
+
+  val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
+  (** Same with four lists, folding on the left *)
+
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  (* [@@ocaml.deprecated "Same as [fold_left_map]"] *)
   (** @deprecated Same as [fold_left_map] *)
 
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index fb65a8639..c8c4c2dad 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -38,9 +38,8 @@ let start_deriving f suchthat lemma =
         let f_type = EConstr.Unsafe.to_constr f_type in
         let ef = EConstr.Unsafe.to_constr ef in
         let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
-        let evdref = ref sigma in
-        let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
-        TCons ( env' , !evdref , suchthat , (fun sigma _ ->
+        let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in
+        TCons ( env' , sigma , suchthat , (fun sigma _ ->
         TNil sigma))))))
     in
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9e22ad306..357755e46 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -158,8 +158,8 @@ let build_newrecursive
       (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
         let arityc = Constrexpr_ops.mkCProdN bl arityc in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
-	let evdref = ref (Evd.from_env env0) in
-	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
+        let evd = Evd.from_env env0 in
+        let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
         let open Context.Named.Declaration in
         (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 766adfc63..363ad5dfc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1427,7 +1427,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
-    let evmap, env = Pfedit.get_current_context () in
+    let evd, env = Pfedit.get_current_context () in
     Lemmas.start_proof thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
       ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t ->
 	| ConstRef c -> is_opaque_constant c
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
-    let evmap, env = Pfedit.get_current_context () in
-    let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
+    let evd, env = Pfedit.get_current_context () in
+    let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
        ~sign:(Environ.named_context_val env)
-       evmap
+       evd
        (EConstr.of_constr equation_lemma_type)
        (Lemmas.mk_hook (fun _ _ -> ()));
      ignore (by
@@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let open Constr in
   let open CVars in
   let env = Global.env() in
-  let evd = ref (Evd.from_env env) in
-  let function_type = interp_type_evars env evd type_of_f in
+  let evd = Evd.from_env env in
+  let evd, function_type = interp_type_evars env evd type_of_f in
   let function_type = EConstr.Unsafe.to_constr function_type in
   let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
-  let ty = interp_type_evars env evd ~impls:rec_impls eq in
+  let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
   let ty = EConstr.Unsafe.to_constr ty in
-  let evm, nf = Evarutil.nf_evars_and_universes !evd in
+  let evd, nf = Evarutil.nf_evars_and_universes evd in
   let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
   let function_type = nf function_type in
   let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
@@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
-    let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+    let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
     declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
   in
   (* Refresh the global universes, now including those of _F *)
-  let evm = Evd.from_env (Global.env ()) in
+  let evd = Evd.from_env (Global.env ()) in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
   let relation, evuctx =
-    interp_constr env_with_pre_rec_args evm r
+    interp_constr env_with_pre_rec_args evd r
   in
-  let evm = Evd.from_ctx evuctx in
+  let evd = Evd.from_ctx evuctx in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
@@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and functional_ref = destConst (constr_of_global functional_ref)
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
-	functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
+        functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation);
       Flags.if_verbose
         msgnl (h 1 (Ppconstr.pr_id function_name ++
 			 spc () ++ str"is defined" )++ fnl () ++
@@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       term_id
       using_lemmas
       (List.length res_vars)
-      evm (Lemmas.mk_hook hook))
+      evd (Lemmas.mk_hook hook))
     ()
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ae3577ed..01065868d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -249,11 +249,11 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 
 let add_inversion_lemma_exn na com comsort bool tac =
   let env = Global.env () in
-  let evd = ref (Evd.from_env env) in
-  let c = Constrintern.interp_type_evars env evd com in
-  let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in
+  let sigma = Evd.from_env env in
+  let sigma, c = Constrintern.interp_type_evars env sigma com in
+  let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in
   try
-    add_inversion_lemma na env evd c sort bool tac
+    add_inversion_lemma na env sigma c sort bool tac
   with
     |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
 	  user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/vernac/classes.ml b/vernac/classes.ml
index fd43c6041..efaf6c0c0 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -82,18 +82,18 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
 let type_ctx_instance env sigma ctx inst subst =
   let open Vars in
-  let rec aux (subst, instctx) l = function
+  let rec aux (sigma, subst, instctx) l = function
     decl :: ctx ->
       let t' = substl subst (RelDecl.get_type decl) in
-      let c', l =
+      let (sigma, c'), l =
 	match decl with
         | LocalAssum _ -> interp_casted_constr_evars env sigma (List.hd l) t', List.tl l
-	| LocalDef (_,b,_) -> substl subst b, l
+        | LocalDef (_,b,_) -> (sigma, substl subst b), l
       in
       let d = RelDecl.get_name decl, Some c', t' in
-	aux (c' :: subst, d :: instctx) l ctx
-    | [] -> subst
-  in aux (subst, []) inst (List.rev ctx)
+        aux (sigma, c' :: subst, d :: instctx) l ctx
+    | [] -> sigma, subst
+  in aux (sigma, subst, []) inst (List.rev ctx)
 
 let id_of_class cl =
   match cl.cl_impl with
@@ -153,10 +153,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
     else tclass 
   in
   let sigma, k, u, cty, ctx', ctx, len, imps, subst =
-    let _evd = ref sigma in
-    let impls, ((env', ctx), imps) = interp_context_evars env _evd ctx in
-    let c', imps' = interp_type_evars_impls ~impls env' _evd tclass in
-    let sigma = !_evd in
+    let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
+    let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
     let len = List.length ctx in
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum sigma c' in
@@ -225,9 +223,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
         | None ->
           (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
 	| Some (Inr term) ->
-            let _evd = ref sigma in
-            let c = interp_casted_constr_evars env' _evd term cty in
-            Some (Inr (c, subst)), !_evd
+            let sigma, c = interp_casted_constr_evars env' sigma term cty in
+            Some (Inr (c, subst)), sigma
 	| Some (Inl props) ->
 	    let get_id =
 	      function
@@ -265,9 +262,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 		unbound_method env' k.cl_impl (get_id n)
               | _ ->
                 let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
-                let _evd = ref sigma in
-                let r_term = type_ctx_instance (push_rel_context ctx' env') _evd kcl_props props subst in
-                Some (Inl r_term), !_evd
+                let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in
+                Some (Inl res), sigma
       in
       let term, termtype =
 	match subst with
@@ -367,9 +363,7 @@ let named_of_rel_context l =
 let context poly l =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let _evd = ref sigma in
-  let _, ((env', fullctx), impls) = interp_context_evars env _evd l in
-  let sigma = !_evd in
+  let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in
   (* Note, we must use the normalized evar from now on! *)
   let sigma,_ = Evarutil.nf_evars_and_universes sigma in
   let ce t = Pretyping.check_evars env Evd.empty sigma t in
diff --git a/vernac/command.ml b/vernac/command.ml
index 64412b20f..837785ff0 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -91,33 +91,32 @@ let warn_implicits_in_term =
 let interp_definition pl bl poly red_option c ctypopt =
   let env = Global.env() in
   let evd, decl = Univdecls.interp_univ_decl_opt env pl in
-  let evdref = ref evd in
-  let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
+  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
   let nb_args = Context.Rel.nhyps ctx in
-  let imps,ce =
+  let evd,imps,ce =
     match ctypopt with
       None ->
-        let subst = evd_comb0 Evd.nf_univ_variables evdref in
+        let evd, subst = Evd.nf_univ_variables evd in
 	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
-	let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
+        let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in
 	let c = EConstr.Unsafe.to_constr c in
-        let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
+        let evd,nf = Evarutil.nf_evars_and_universes evd in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
-        let () = evdref := Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly !evdref decl in
-        imps1@(Impargs.lift_implicits nb_args imps2),
+        let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
+        let evd = Evd.restrict_universe_context evd vars in
+        let uctx = Evd.check_univ_decl ~poly evd decl in
+        evd, imps1@(Impargs.lift_implicits nb_args imps2),
           definition_entry ~univs:uctx body
     | Some ctyp ->
-        let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
-        let subst = evd_comb0 Evd.nf_univ_variables evdref in
+        let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in
+        let evd, subst = Evd.nf_univ_variables evd in
 	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
-	let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
+        let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
 	let c = EConstr.Unsafe.to_constr c in
-	let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+        let evd, nf = Evarutil.nf_evars_and_universes evd in
 	let body = nf (it_mkLambda_or_LetIn c ctx) in
 	let ty = EConstr.Unsafe.to_constr ty in
 	let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
@@ -130,15 +129,15 @@ let interp_definition pl bl poly red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
-        let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in
+        let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
+        let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in
         let vars = Univ.LSet.union bodyvars tyvars in
-        let () = evdref := Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly !evdref decl in
-        imps1@(Impargs.lift_implicits nb_args impsty),
+        let evd = Evd.restrict_universe_context evd vars in
+        let uctx = Evd.check_univ_decl ~poly evd decl in
+        evd, imps1@(Impargs.lift_implicits nb_args impsty),
           definition_entry ~types:typ ~univs:uctx body
   in
-  (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
+  (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
 
 let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
@@ -232,11 +231,11 @@ match local with
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let interp_assumption evdref env impls bl c =
+let interp_assumption sigma env impls bl c =
   let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
-  let ty, impls = interp_type_evars_impls env evdref ~impls c in
+  let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
   let ty = EConstr.Unsafe.to_constr ty in
-  (ty, impls)
+  sigma, (ty, impls)
 
 (* When monomorphic the universe constraints are declared with the first declaration only. *)
 let next_uctx =
@@ -285,10 +284,7 @@ let do_assumptions kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let udecl, l = process_assumptions_udecls kind l in
-  let evdref, udecl =
-    let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in
-    ref evd, udecl
-  in
+  let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
   let l =
     if pi2 kind (* poly *) then
       (* Separate declarations so that A B : Type puts A and B in different levels. *)
@@ -299,29 +295,29 @@ let do_assumptions kind nl l =
     else l
   in
   (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
-  let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) ->
-    let t,imps = interp_assumption evdref env ienv [] c in
+  let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
+    let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
     let env =
       push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun (_,id) ienv ->
       let impls = compute_internalization_data env Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
-      ((env,ienv),((is_coe,idl),t,imps)))
-    (env,empty_internalization_env) l
+      ((sigma,env,ienv),((is_coe,idl),t,imps)))
+    (sigma,env,empty_internalization_env) l
   in
-  let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
+  let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in
   (* The universe constraints come from the whole telescope. *)
-  let evd = Evd.nf_constraints evd in
-  let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in
+  let sigma = Evd.nf_constraints sigma in
+  let nf_evar c = EConstr.to_constr sigma (EConstr.of_constr c) in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
       let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
-  let evd = Evd.restrict_universe_context evd uvars in
-  let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in
-  let ubinders = Evd.universe_binders evd in
+  let sigma = Evd.restrict_universe_context sigma uvars in
+  let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in
+  let ubinders = Evd.universe_binders sigma in
   pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
       let t = replace_vars subst t in
       let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
@@ -375,8 +371,8 @@ let check_all_names_different indl =
   | [] -> ()
   | _ -> raise (InductiveError (SameNamesOverlap l))
 
-let mk_mltype_data evdref env assums arity indname =
-  let is_ml_type = is_sort env !evdref (EConstr.of_constr arity) in
+let mk_mltype_data sigma env assums arity indname =
+  let is_ml_type = is_sort env sigma (EConstr.of_constr arity) in
   (is_ml_type,indname,assums)
 
 let prepare_param = function
@@ -400,40 +396,43 @@ let rec check_anonymous_type ind =
     | GCast (e, _) -> check_anonymous_type e
     | _ -> false
 
-let make_conclusion_flexible evdref ty poly =
+let make_conclusion_flexible sigma ty poly =
   if poly && Term.isArity ty then
     let _, concl = Term.destArity ty in
       match concl with
       | Type u -> 
         (match Univ.universe_level u with
         | Some u -> 
-	  evdref := Evd.make_flexible_variable !evdref ~algebraic:true u
-	| None -> ())
-      | _ -> ()
-  else () 
-	
-let is_impredicative env u = 
+          Evd.make_flexible_variable sigma ~algebraic:true u
+        | None -> sigma)
+      | _ -> sigma
+  else sigma
+
+let is_impredicative env u =
   u = Prop Null || (is_impredicative_set env && u = Prop Pos)
 
-let interp_ind_arity env evdref ind =
+let interp_ind_arity env sigma ind =
   let c = intern_gen IsType env ind.ind_arity in
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
-  let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in
-  evdref := evd;
+  let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
   let pseudo_poly = check_anonymous_type c in
-  let () = if not (Reductionops.is_arity env !evdref t) then
+  let () = if not (Reductionops.is_arity env sigma t) then
     user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
   in
   let t = EConstr.Unsafe.to_constr t in
-    t, pseudo_poly, impls
+  sigma, (t, pseudo_poly, impls)
 
-let interp_cstrs evdref env impls mldata arity ind =
+let interp_cstrs env sigma impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
   (* Complete conclusions of constructor types if given in ML-style syntax *)
   let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
   (* Interpret the constructor types *)
-  let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in
-    (cnames, ctyps'', cimpls)
+  let sigma, (ctyps'', cimpls) =
+    on_snd List.split @@
+    List.fold_left_map (fun sigma l ->
+        on_snd (on_fst EConstr.Unsafe.to_constr) @@
+        interp_type_evars_impls env sigma ~impls l) sigma ctyps' in
+  sigma, (cnames, ctyps'', cimpls)
 
 let sign_level env evd sign =
   fst (List.fold_right
@@ -461,7 +460,7 @@ let is_flexible_sort evd u =
   | Some l -> Evd.is_flexible_level evd l
   | None -> false
 
-let inductive_levels env evdref poly arities inds =
+let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) -> 
     if a = Prop Null then None
@@ -480,11 +479,11 @@ let inductive_levels env evdref poly arities inds =
 	let minlev =
 	  (** Indices contribute. *)
 	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
-	    let ilev = sign_level env !evdref ctx in
+            let ilev = sign_level env evd ctx in
 	      Univ.sup ilev minlev)
 	  else minlev
 	in
-	let clev = extract_level env !evdref minlev tys in
+        let clev = extract_level env evd minlev tys in
 	  (clev, minlev, len)) inds destarities)
   in
   (* Take the transitive closure of the system of constructors *)
@@ -529,8 +528,8 @@ let inductive_levels env evdref poly arities inds =
 	  else Evd.set_eq_sort env evd (Type cu) du
 	in
 	  (evd, arity :: arities))
-    (!evdref,[]) (Array.to_list levels') destarities sizes
-  in evdref := evd; List.rev arities
+    (evd,[]) (Array.to_list levels') destarities sizes
+  in evd, List.rev arities
 
 let check_named (loc, na) = match na with
 | Name _ -> ()
@@ -551,20 +550,19 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   List.iter check_param paramsl;
   let env0 = Global.env() in
   let pl = (List.hd indl).ind_univs in
-  let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
-  let evdref = ref evd in
-  let impls, ((env_params, ctx_params), userimpls) =
-    interp_context_evars env0 evdref paramsl
+  let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let sigma, (impls, ((env_params, ctx_params), userimpls)) =
+    interp_context_evars env0 sigma paramsl
   in
   let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-      
+
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
   let params = List.map (RelDecl.get_name %> Name.get_id) assums in
 
   (* Interpret the arities *)
-  let arities = List.map (interp_ind_arity env_params evdref) indl in
+  let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
 
   let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in
   let env_ar = push_types env0 indnames fullarities in
@@ -576,36 +574,34 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
   let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in
   let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in
-  let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
+  let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
 
-  let constructors =
+  let sigma, constructors =
     Metasyntax.with_syntax_protection (fun () ->
      (* Temporary declaration of notations and scopes *)
      List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
      (* Interpret the constructor types *)
-     List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
+     List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl)
      () in
 
   (* Try further to solve evars, and instantiate them *)
-  let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in
-  evdref := sigma;
+  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
   (* Compute renewed arities *)
-  let nf,_ = e_nf_evars_and_universes evdref in
+  let sigma, nf = nf_evars_and_universes sigma in
   let arities = List.map nf arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
-  let _ = List.iter2 (fun ty poly -> make_conclusion_flexible evdref ty poly) arities aritypoly in
-  let arities = inductive_levels env_ar_params evdref poly arities constructors in
-  let nf',_ = e_nf_evars_and_universes evdref in
+  let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
+  let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
+  let sigma, nf' = nf_evars_and_universes sigma in
   let nf x = nf' (nf x) in
   let arities = List.map nf' arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
   let ctx_params = Context.Rel.map nf ctx_params in
-  let evd = !evdref in
-  let uctx = Evd.check_univ_decl ~poly evd decl in
-  List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
-  Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
+  let uctx = Evd.check_univ_decl ~poly sigma decl in
+  List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
+  Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
-    List.iter (fun c -> check_evars env_ar_params Evd.empty evd (EConstr.of_constr c)) ctyps)
+    List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps)
     constructors;
 
   (* Build the inductive entries *)
@@ -642,8 +638,8 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
     }
   in
   (if poly && cum then
-      Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
-   else mind_ent), Evd.universe_binders evd, impls
+      Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent
+   else mind_ent), Evd.universe_binders sigma, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -830,23 +826,22 @@ type structured_fixpoint_expr = {
   fix_type : constr_expr
 }
 
-let interp_fix_context env evdref isfix fix =
+let interp_fix_context env sigma isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
-  let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in
+  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars env sigma before in
+  let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
-    ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
+  sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
-let interp_fix_ccl evdref impls (env,_) fix =
-  let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in
-  (c, impl)
+let interp_fix_ccl sigma impls (env,_) fix =
+  interp_type_evars_impls ~impls env sigma fix.fix_type
 
-let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
+let interp_fix_body env_rec sigma impls (_,ctx) fix ccl =
   let open EConstr in
-  Option.map (fun body ->
+  Option.cata (fun body ->
     let env = push_rel_context ctx env_rec in
-    let body = interp_casted_constr_evars env evdref ~impls body ccl in
-    it_mkLambda_or_LetIn body ctx) fix.fix_body
+    let sigma, body = interp_casted_constr_evars env sigma ~impls body ccl in
+    sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body
 
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
@@ -883,56 +878,58 @@ let fixsub_module = subtac_dir @ ["Wf"]
 let tactics_module = subtac_dir @ ["Tactics"]
 
 let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant  dir s evdref =
-  let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s)
-  in evdref := sigma; c
+let init_constant dir s sigma =
+  Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
 
 let make_ref l s = init_reference l s
 let fix_proto = init_constant tactics_module "fix_proto"
 let fix_sub_ref = make_ref fixsub_module "Fix_sub"
 let measure_on_R_ref = make_ref fixsub_module "MR"
 let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let mkSubset evdref name typ prop =
+let mkSubset sigma name typ prop =
   let open EConstr in
-  mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ,
-	 [| typ; mkLambda (name, typ, prop) |])
+  let sigma, h_term = Evarutil.new_global sigma (delayed_force build_sigma).typ in
+  sigma, mkApp (h_term, [| typ; mkLambda (name, typ, prop) |])
+
 let sigT = Lazy.from_fun build_sigma_type
 
 let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
 let lt_ref = make_qref "Init.Peano.lt"
 
-let rec telescope evdref l =
+let rec telescope sigma l =
   let open EConstr in
   let open Vars in
   match l with
   | [] -> assert false
-  | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1
+  | [LocalAssum (n, t)] ->
+    sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1
   | LocalAssum (n, t) :: tl ->
-      let ty, tys, (k, constr) =
+      let sigma, ty, tys, (k, constr) =
 	List.fold_left
-	  (fun (ty, tys, (k, constr)) decl ->
+          (fun (sigma, ty, tys, (k, constr)) decl ->
             let t = RelDecl.get_type decl in
             let pred = mkLambda (RelDecl.get_name decl, t, ty) in
-	    let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in
-	    let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in
+            let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in
+            let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in
 	    let sigty = mkApp (ty, [|t; pred|]) in
 	    let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
-	      (sigty, pred :: tys, (succ k, intro)))
-	  (t, [], (2, mkRel 1)) tl
+              (sigma, sigty, pred :: tys, (succ k, intro)))
+          (sigma, t, [], (2, mkRel 1)) tl
       in
-      let (last, subst) = List.fold_right2
-        (fun pred decl (prev, subst) ->
+      let sigma, last, subst = List.fold_right2
+        (fun pred decl (sigma, prev, subst) ->
           let t = RelDecl.get_type decl in
-	  let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in
-	  let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in
+          let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in
+          let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in
 	  let proj1 = applist (p1, [t; pred; prev]) in
 	  let proj2 = applist (p2, [t; pred; prev]) in
-	    (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
-	(List.rev tys) tl (mkRel 1, [])
-      in ty, (LocalDef (n, last, t) :: subst), constr
+            (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
+        (List.rev tys) tl (sigma, mkRel 1, [])
+      in sigma, ty, (LocalDef (n, last, t) :: subst), constr
 
-  | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in
-      ty, (LocalDef (n, b, t) :: subst), lift 1 term
+  | LocalDef (n, b, t) :: tl ->
+    let sigma, ty, subst, term = telescope sigma tl in
+    sigma, ty, (LocalDef (n, b, t) :: subst), lift 1 term
 
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
@@ -943,56 +940,59 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
-  let evdref = ref evd in
-  let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
+  let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+  let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
-  let top_arity = interp_type_evars top_env evdref arityc in
+  let sigma, top_arity = interp_type_evars top_env sigma arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
-  let argtyp, letbinders, make = telescope evdref binders_rel in
+  let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = LocalAssum (Name argname, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
-  let rel, _ = interp_constr_evars_impls env evdref r in
-  let relty = Typing.unsafe_type_of env !evdref rel in
+  let sigma, (rel, _) = interp_constr_evars_impls env sigma r in
+  let relty = Typing.unsafe_type_of env sigma rel in
   let relargty =
     let error () =
       user_err ?loc:(constr_loc r)
                ~hdr:"Command.build_wellfounded"
-		    (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
+                    (Printer.pr_econstr_env env sigma rel ++ str " is not an homogeneous binary relation.")
     in
       try
-	let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
-	  match ctx, EConstr.kind !evdref ar with
+        let ctx, ar = Reductionops.splay_prod_n env sigma 2 relty in
+          match ctx, EConstr.kind sigma ar with
 	  | [LocalAssum (_,t); LocalAssum (_,u)], Sort s
-	      when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t
+              when Sorts.is_prop (ESorts.kind sigma s) && Reductionops.is_conv env sigma t u -> t
 	  | _, _ -> error ()
       with e when CErrors.noncritical e -> error ()
   in
-  let measure = interp_casted_constr_evars binders_env evdref measure relargty in
-  let wf_rel, wf_rel_fun, measure_fn =
+  let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in
+  let sigma, wf_rel, wf_rel_fun, measure_fn =
     let measure_body, measure =
       it_mkLambda_or_LetIn measure letbinders,
       it_mkLambda_or_LetIn measure binders
     in
-    let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in
+    let sigma, comb = Evarutil.new_global sigma (delayed_force measure_on_R_ref) in
     let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
     let wf_rel_fun x y =
       mkApp (rel, [| subst1 x measure_body;
  		     subst1 y measure_body |])
-    in wf_rel, wf_rel_fun, measure
+    in sigma, wf_rel, wf_rel_fun, measure
   in
-  let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in
+  let sigma, wf_term = well_founded sigma in
+  let wf_proof = mkApp (wf_term, [| argtyp ; wf_rel |]) in
   let argid' = Id.of_string (Id.to_string argname ^ "'") in
-  let wfarg len = LocalAssum (Name argid',
-                              mkSubset evdref (Name argid') argtyp
-				       (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+  let wfarg sigma len =
+    let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in
+    sigma, LocalAssum (Name argid', ss_term)
+  in
+  let sigma, intern_bl =
+    let sigma, wfa = wfarg sigma 1 in
+    sigma, wfa :: [arg]
   in
-  let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
-  let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in
+  let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in
   let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1001,82 +1001,90 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let intern_arity = substl [projection] top_arity_let in
   (* substitute the projection of wfarg for something,
      now intern_arity is in wfarg :: arg *)
-  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
+  let sigma, wfa = wfarg sigma 1 in
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in
   let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
-  let curry_fun =
+  let sigma, curry_fun =
     let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
-    let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in
+    let sigma, intro = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.intro in
     let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
     let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
     let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
     let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
-      LocalDef (Name recname, body, ty)
+    sigma, LocalDef (Name recname, body, ty)
   in
   let fun_bl = intern_fun_binder :: [arg] in
   let lift_lets = lift_rel_context 1 letbinders in
-  let intern_body =
+  let sigma, intern_body =
     let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
     let (r, l, impls, scopes) =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls 
     in
     let newimpls = Id.Map.singleton recname
-      (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
-       scopes @ [None]) in
-      interp_casted_constr_evars (push_rel_context ctx env) evdref
-        ~impls:newimpls body (lift 1 top_arity)
+        (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+         scopes @ [None]) in
+    interp_casted_constr_evars (push_rel_context ctx env) sigma
+      ~impls:newimpls body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
   let prop = mkLambda (Name argname, argtyp, top_arity_let) in
-  let def =
-    mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref),
-	  [| argtyp ; wf_rel ;
-	     Evarutil.e_new_evar env evdref
-	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
-	     prop |])
+  (* XXX: Previous code did parallel evdref update, so possible old
+     weak ordering semantics may bite here. *)
+  let sigma, def =
+    let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in
+    let sigma, h_e_term = Evarutil.new_evar env sigma
+        ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
+    sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
   in
-  let def = Typing.e_solve_evars env evdref def in
-  let _ = evdref := Evarutil.nf_evar_map !evdref in
+  let _evd = ref sigma in
+  let def = Typing.e_solve_evars env _evd def in
+  let sigma = !_evd in
+  let sigma = Evarutil.nf_evar_map sigma in
   let def = mkApp (def, [|intern_body_lam|]) in
-  let binders_rel = nf_evar_context !evdref binders_rel in
-  let binders = nf_evar_context !evdref binders in
-  let top_arity = Evarutil.nf_evar !evdref top_arity in
+  let binders_rel = nf_evar_context sigma binders_rel in
+  let binders = nf_evar_context sigma binders in
+  let top_arity = Evarutil.nf_evar sigma top_arity in
   let hook, recname, typ =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
-      let hook l gr _ = 
-        let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
+      (* XXX: Mutating the evar_map in the hook! *)
+      (* XXX: Likely the sigma is out of date when the hook is called .... *)
+      let hook sigma l gr _ =
+        let sigma, h_body = Evarutil.new_global sigma gr in
+        let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
         let ty = EConstr.Unsafe.to_constr ty in
-        let univs = Evd.check_univ_decl ~poly !evdref decl in
+        let univs = Evd.check_univ_decl ~poly sigma decl in
         (*FIXME poly? *)
-        let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in
+        let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
         (** FIXME: include locality *)
         let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
         let gr = ConstRef c in
-        let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in
+        let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr [impls]
       in
       let typ = it_mkProd_or_LetIn top_arity binders in
-	hook, name, typ
-    else 
+      hook, name, typ
+    else
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook l gr _ = 
+      let hook sigma l gr _ =
 	if Impargs.is_implicit_args () || not (List.is_empty impls) then
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
   in
-  let hook = Lemmas.mk_hook hook in
-  let fullcoqc = EConstr.to_constr !evdref def in
-  let fullctyp = EConstr.to_constr !evdref typ in
-  Obligations.check_evars env !evdref;
-  let evars, _, evars_def, evars_typ = 
-    Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
+  (* XXX: Capturing sigma here... bad bad *)
+  let hook = Lemmas.mk_hook (hook sigma) in
+  let fullcoqc = EConstr.to_constr sigma def in
+  let fullctyp = EConstr.to_constr sigma typ in
+  Obligations.check_evars env sigma;
+  let evars, _, evars_def, evars_typ =
+    Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
   in
-  let ctx = Evd.evar_universe_context !evdref in
+  let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
 	     evars_typ ctx evars ~hook)
 
@@ -1097,31 +1105,36 @@ let interp_recursive isfix fixl notations =
 	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
 	     user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
 	   Some us) fixl None in
-  let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in
-  let evdref = ref evd in
-  let fixctxs, fiximppairs, fixannots =
-    List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
+  let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in
+  let sigma, (fixctxs, fiximppairs, fixannots) =
+    on_snd List.split3 @@
+      List.fold_left_map (fun sigma -> interp_fix_context env sigma isfix) sigma fixl in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
-  let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
+  let sigma, (fixccls,fixcclimps) =
+    on_snd List.split @@
+      List.fold_left3_map interp_fix_ccl sigma fixctximpenvs fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
-  let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in
+  let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
   let fiximps = List.map3
     (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
     fixctximps fixcclimps fixctxs in
-  let rec_sign =
+  let sigma, rec_sign =
     List.fold_left2
-      (fun env' id t ->
- 	 if Flags.is_program_mode () then
-	   let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
-	   let fixprot =
-	     try 
-	       let app = mkApp (fix_proto evdref, [|sort; t|]) in
-		 Typing.e_solve_evars env evdref app
-	     with e  when CErrors.noncritical e -> t
-	   in
-	     LocalAssum (id,fixprot) :: env'
-	 else LocalAssum (id,t) :: env')
-      [] fixnames fixtypes
+      (fun (sigma, env') id t ->
+         if Flags.is_program_mode () then
+           let sigma, sort = Typing.type_of ~refresh:true env sigma t in
+           let sigma, fixprot =
+             try
+               let sigma, h_term = fix_proto sigma in
+               let app = mkApp (h_term, [|sort; t|]) in
+               let _evd = ref sigma in
+               let res = Typing.e_solve_evars env _evd app in
+               !_evd, res
+             with e when CErrors.noncritical e -> sigma, t
+           in
+           sigma, LocalAssum (id,fixprot) :: env'
+         else sigma, LocalAssum (id,t) :: env')
+      (sigma,[]) fixnames fixtypes
   in
   let env_rec = push_named_context rec_sign env in
 
@@ -1130,24 +1143,24 @@ let interp_recursive isfix fixl notations =
   let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
-  let fixdefs =
+  let sigma, fixdefs =
     Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
-      List.map4
-	(fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls))
-	fixctximpenvs fixctxs fixl fixccls)
+      List.fold_left4_map
+        (fun sigma fixctximpenv -> interp_fix_body env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
+        sigma fixctximpenvs fixctxs fixl fixccls)
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd = solve_unif_constraints_with_heuristics env_rec !evdref in
-  let evd, nf = nf_evars_and_universes evd in
+  let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
+  let sigma, nf = nf_evars_and_universes sigma in
   let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
   let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+  (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
   check_evars_are_solved env evd Evd.empty;
@@ -1170,7 +1183,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
@@ -1205,7 +1218,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 200c2260e..27a680b9b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -13,12 +13,10 @@ open CErrors
 open Util
 open Pp
 open Names
-open Term
 open Constr
 open Declarations
 open Declareops
 open Entries
-open Environ
 open Nameops
 open Globnames
 open Decls
@@ -88,28 +86,28 @@ let adjust_guardness_conditions const = function
 		(mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
 
-let find_mutually_recursive_statements thms =
+let find_mutually_recursive_statements sigma thms =
     let n = List.length thms in
     let inds = List.map (fun (id,(t,impls)) ->
-      let (hyps,ccl) = decompose_prod_assum t in
+      let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in
       let x = (id,(t,impls)) in
-      let whnf_hyp_hds = map_rel_context_in_env
-        (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c))))
+      let whnf_hyp_hds = EConstr.map_rel_context_in_env
+        (fun env c -> fst (Reductionops.whd_all_stack env sigma c))
         (Global.env()) hyps in
       let ind_hyps =
         List.flatten (List.map_i (fun i decl ->
           let t = RelDecl.get_type decl in
-          match Constr.kind t with
+          match EConstr.kind sigma t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
                 mind.mind_finite <> Decl_kinds.CoFinite ->
               [ind,x,i]
           | _ ->
-              []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in
+              []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
       let ind_ccl =
-        let cclenv = push_rel_context hyps (Global.env()) in
-        let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in
-        match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with
+        let cclenv = EConstr.push_rel_context hyps (Global.env()) in
+        let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
+        match EConstr.kind sigma whnf_ccl with
         | Ind ((kn,_ as ind),u) when
               let mind = Global.lookup_mind kn in
               Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
@@ -163,14 +161,14 @@ let find_mutually_recursive_statements thms =
     in
     (finite,guard,None), ordered_inds
 
-let look_for_possibly_mutual_statements = function
+let look_for_possibly_mutual_statements sigma = function
   | [id,(t,impls)] ->
       (* One non recursively proved theorem *)
       None,[id,(t,impls)],None
   | _::_ as thms ->
     (* More than one statement and/or an explicit decreasing mark: *)
     (* we look for a common inductive hyp or a common coinductive conclusion *)
-    let recguard,ordered_inds = find_mutually_recursive_statements thms in
+    let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in
     let thms = List.map pi2 ordered_inds in
     Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
   | [] -> anomaly (Pp.str "Empty list of theorems.")
@@ -377,7 +375,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with
+    match List.map (fun (id,(t,_)) -> (id,t)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -385,11 +383,11 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with 
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
+    in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization kind ctx decl recguard thms snl hook =
+let start_proof_with_initialization kind sigma decl recguard thms snl hook =
   let intro_tac (_, (_, (ids, _))) =
     Tacticals.New.tclMAP (function
     | Name id -> Tactics.intro_mustbe_force id
@@ -424,16 +422,15 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
           if List.is_empty other_thms then [] else
             (* there are several theorems defined mutually *)
             let body,opaq = retrieve_first_recthm ctx ref in
-            let subst = Evd.evar_universe_context_subst ctx in
-            let norm c = Universes.subst_opt_univs_constr subst c in
-            let body = Option.map norm body in
+            let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
+            let body = Option.map EConstr.of_constr body in
             let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
             List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
@@ -442,22 +439,24 @@ let start_proof_com ?inference_hook kind thms hook =
     match decl with
     | None -> Evd.from_env env0, Univdecls.default_univ_decl
     | Some decl ->
-       Univdecls.interp_univ_decl_opt env0 (snd decl) in
-  let evdref = ref evd in
-  let thms = List.map (fun (sopt,(bl,t)) ->
-    let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
-    let t', imps' = interp_type_evars_impls ~impls env evdref t in
+      Univdecls.interp_univ_decl_opt env0 (snd decl) in
+  let evd, thms = List.fold_left_map (fun evd (sopt,(bl,t)) ->
+    let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
+    let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
     let flags = all_and_fail_flags in
     let flags = { flags with use_hook = inference_hook } in
-    evdref := solve_remaining_evars flags env !evdref Evd.empty;
+    let evd = solve_remaining_evars flags env evd Evd.empty in
     let ids = List.map RelDecl.get_name ctx in
-      (compute_proof_name (pi1 kind) sopt,
-      (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
-       (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
-    thms in
-  let recguard,thms,snl = look_for_possibly_mutual_statements thms in
-  let evd, nf = Evarutil.nf_evars_and_universes !evdref in
-  let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+    (* XXX: The nf_evar is critical !! *)
+    evd, (compute_proof_name (pi1 kind) sopt,
+          (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
+           (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
+      evd thms in
+  let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
+  let evd, _nf = Evarutil.nf_evars_and_universes evd in
+  (* XXX: This nf_evar is critical too!! We are normalizing twice if
+     you look at the previous lines... *)
+  let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
   let () =
     let open Misctypes in
     if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
@@ -470,7 +469,6 @@ let start_proof_com ?inference_hook kind thms hook =
   in
     start_proof_with_initialization kind evd decl recguard thms snl hook
 
-
 (* Saving a proof *)
 
 let keep_admitted_vars = ref true
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a4854b4a6..ca92e856b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Decl_kinds
 
 type 'a declaration_hook
@@ -37,11 +36,11 @@ val start_proof_com :
   goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
-val start_proof_with_initialization : 
+val start_proof_with_initialization :
   goal_kind -> Evd.evar_map -> Univdecls.universe_decl ->
   (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t (* name of thm *) *
-     (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+     (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
 val universe_proof_terminator :
diff --git a/vernac/record.ml b/vernac/record.ml
index 1cdc538b5..d97a5149d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -60,23 +60,25 @@ let _ =
       optread  = (fun () -> !typeclasses_unique);
       optwrite = (fun b -> typeclasses_unique := b); }
 
-let interp_fields_evars env evars impls_env nots l =
+let interp_fields_evars env sigma impls_env nots l =
   List.fold_left2
-    (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
-      let t', impl = interp_type_evars_impls env evars ~impls t in
-      let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
+    (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) ->
+      let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
+      let sigma, b' =
+        Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
+                      interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in
       let impls =
 	match i with
 	| Anonymous -> impls
-	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr !evars t') impl) impls
+        | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls
       in
       let d = match b' with
 	      | None -> LocalAssum (i,t')
 	      | Some b' -> LocalDef (i,b',t')
       in
       List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
-      (EConstr.push_rel d env, impl :: uimpls, d::params, impls))
-    (env, [], [], impls_env) nots l
+      (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
+    (env, sigma, [], [], impls_env) nots l
 
 let compute_constructor_level evars env l =
   List.fold_right (fun d (env, univ) ->
@@ -97,10 +99,9 @@ let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let env0 = Global.env () in
-  let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
-  let evars = ref evd in
-  let _ = 
-    let error bk (loc, name) = 
+  let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let _ =
+    let error bk (loc, name) =
       match bk, name with
       | Default _, Anonymous ->
         user_err ?loc ~hdr:"record" (str "Record parameters must be named")
@@ -112,63 +113,65 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
            | CLocalPattern (loc,(_,_)) ->
               Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
   in 
-  let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
-  let typ, sort, template = match t with
+  let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
+  let sigma, typ, sort, template = match t with
     | Some t -> 
        let env = EConstr.push_rel_context newps env0 in
        let poly =
          match t with
          | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
-       let s = interp_type_evars env evars ~impls:empty_internalization_env t in
-       let sred = Reductionops.whd_all env !evars s in
-	 (match EConstr.kind !evars sred with
+       let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in
+       let sred = Reductionops.whd_all env sigma s in
+         (match EConstr.kind sigma sred with
 	 | Sort s' ->
-            let s' = EConstr.ESorts.kind !evars s' in
+            let s' = EConstr.ESorts.kind sigma s' in
 	    (if poly then
-               match Evd.is_sort_variable !evars s' with
-	       | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; 
-	                  s, s', true
-	       | None -> s, s', false
-             else s, s', false)
+               match Evd.is_sort_variable sigma s' with
+               | Some l ->
+                 let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
+                 sigma, s, s', true
+               | None ->
+                 sigma, s, s', false
+             else sigma, s, s', false)
 	 | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
     | None -> 
       let uvarkind = Evd.univ_flexible_alg in
-      let s = Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars in
-      EConstr.mkSort s, s, true
+      let sigma, s = Evd.new_sort_variable uvarkind sigma in
+      sigma, EConstr.mkSort s, s, true
   in
   let arity = EConstr.it_mkProd_or_LetIn typ newps in
   let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
   let assums = List.filter is_local_assum newps in
   let params = List.map (RelDecl.get_name %> Name.get_id) assums in
   let ty = Inductive (params,(finite != BiFinite)) in
-  let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in
-  let env2,impls,newfs,data =
-    interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
+  let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
+  let env2,sigma,impls,newfs,data =
+    interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
   in
-  let evars =
-    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
-  let typ, evars =
-    let _, univ = compute_constructor_level evars env_ar newfs in
+  let sigma =
+    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in
+  let sigma, typ =
+    let _, univ = compute_constructor_level sigma env_ar newfs in
       if not def && (Sorts.is_prop sort ||
 	(Sorts.is_set sort && is_impredicative_set env0)) then
-	typ, evars
+        sigma, typ
       else
-	let evars = Evd.set_leq_sort env_ar evars (Type univ) sort in
+        let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in
 	if Univ.is_small_univ univ &&
-	   Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars sort) then
+           Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
 	   (* We can assume that the level in aritysort is not constrained
 	       and clear it, if it is flexible *)
-	  EConstr.mkSort (Sorts.sort_of_univ univ),
-	  Evd.set_eq_sort env_ar evars (Prop Pos) sort
-	else typ, evars
+          Evd.set_eq_sort env_ar sigma (Prop Pos) sort,
+          EConstr.mkSort (Sorts.sort_of_univ univ)
+        else sigma, typ
   in
-  let evars, nf = Evarutil.nf_evars_and_universes evars in
-  let newfs = List.map (EConstr.to_rel_decl evars) newfs in
-  let newps = List.map (EConstr.to_rel_decl evars) newps in
-  let typ = EConstr.to_constr evars typ in
-  let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
-  let univs = Evd.check_univ_decl ~poly evars decl in
-  let ubinders = Evd.universe_binders evars in
+  let sigma, _ = Evarutil.nf_evars_and_universes sigma in
+  let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
+  let newps = List.map (EConstr.to_rel_decl sigma) newps in
+  let typ = EConstr.to_constr sigma typ in
+  let ce t = Pretyping.check_evars env0 Evd.empty sigma (EConstr.of_constr t) in
+  let univs = Evd.check_univ_decl ~poly sigma decl in
+  let ubinders = Evd.universe_binders sigma in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
     ubinders, univs, typ, template, imps, newps, impls, newfs