Merge PR #7419: Remove 100 occurrences of Evd.empty

41 files changed, 179 insertions, 114 deletions

diff --git a/dev/base_include b/dev/base_include
index 2f5d8aa84..8d81ca3e0 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -204,7 +204,9 @@ let e s =
    implicit syntax *)
 
 let constr_of_string s = 
-  Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.interp_constr env sigma (parse_constr s);;
 
 (* get the body of a constant *)
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cb1abc4a9..129f171b2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -221,7 +221,9 @@ let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
 let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
-  pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pp (pr_named_context env sigma (named_context_of_val e))
 
 let ppenv e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
diff --git a/engine/termops.ml b/engine/termops.ml
index 053fcc3db..bd07555a5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -98,7 +98,10 @@ let rec pr_constr c = match kind c with
 
 let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
 let print_constr_env env sigma t = !term_printer env sigma t
-let print_constr t = !term_printer (Global.env()) Evd.empty t
+let print_constr t =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  !term_printer env evd t
 let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
@@ -340,7 +343,7 @@ let pr_evar_constraints sigma pbs =
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ protect (print_constr_env env Evd.empty) t2
+      spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2
   in
   prlist_with_sep fnl pr_evconstr pbs
 
@@ -434,27 +437,29 @@ let pr_metaset metas =
 
 let pr_var_decl env decl =
   let open NamedDecl in
+  let evd = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-	let pb = print_constr_env env Evd.empty c in
+        let pb = print_constr_env env evd c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+  let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
 let pr_rel_decl env decl =
   let open RelDecl in
+  let evd = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-	let pb = print_constr_env env Evd.empty c in
+        let pb = print_constr_env env evd c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+  let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 64f165cde..ba69c4185 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -272,7 +272,10 @@ let status force =
 let export_coq_object t = {
   Interface.coq_object_prefix = t.Search.coq_object_prefix;
   Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
+  Interface.coq_object_object =
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Pp.string_of_ppcmds (pr_lconstr_env env sigma t.Search.coq_object_object)
 }
 
 let pattern_of_string ?env s =
@@ -282,7 +285,7 @@ let pattern_of_string ?env s =
     | Some e -> e
   in
   let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-  let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in
+  let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in
   pat
 
 let dirpath_of_string_list s =
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 2db67c299..8aa1e6250 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -237,11 +237,11 @@ let is_rigid env sigma t =
      is_rigid_head sigma t
   | _ -> true
 
-let find_displayed_name_in all avoid na (env, b) =
+let find_displayed_name_in sigma all avoid na (env, b) =
   let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
-  else compute_displayed_name_in Evd.empty flag avoid na b
+  if all then compute_and_force_displayed_name_in sigma flag avoid na b
+  else compute_displayed_name_in sigma flag avoid na b
 
 let compute_implicits_names_gen all env sigma t =
   let open Context.Rel.Declaration in
@@ -249,7 +249,7 @@ let compute_implicits_names_gen all env sigma t =
     let t = whd_all env sigma t in
     match kind sigma t with
     | Prod (na,a,b) ->
-       let na',avoid' = find_displayed_name_in all avoid na (names,b) in
+       let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in
        aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
     | _ -> List.rev names
   in aux env Id.Set.empty [] t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index e51c69136..448881dcf 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -509,7 +509,9 @@ let notation_constr_of_glob_constr nenv a =
 
 let notation_constr_of_constr avoiding t =
   let t = EConstr.of_constr t in
-  let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let t = Detyping.detype Detyping.Now false avoiding env evd t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
diff --git a/interp/reserve.ml b/interp/reserve.ml
index b57103cf2..071248f01 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -112,7 +112,9 @@ let revert_reserved_type t =
     let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
     let t = EConstr.of_constr t in
-    let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 0c752d4a4..2a527da9b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5e0d3e8ee..83fe1fc2f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -230,7 +230,7 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
   with Not_found -> false
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
+  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env @@ Evd.from_env Environ.empty_env
 
 
 exception NoChange
@@ -1099,10 +1099,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
     let get_body const =
       match Global.body_of_constant const with
 	| Some (body, _) ->
+          let env = Global.env () in
+          let sigma = Evd.from_env env in
 	     Tacred.cbv_norm_flags
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-	       (Global.env ())
-	       (Evd.empty)
+               env
+               sigma
 	       (EConstr.of_constr body)
 	| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
     in
@@ -1340,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-                       Reductionops.nf_betaiota (pf_env g) Evd.empty
+                       Reductionops.nf_betaiota (pf_env g) (project g)
 			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90af20b4c..d193e1144 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -38,7 +38,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
   match opt_c with
     | None -> mt ()
     | Some b ->
-      let (_, b) = b (Global.env ()) Evd.empty in
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      let (_, b) = b env evd in
       spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b9d5ebf57..cc92a73f0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -67,7 +67,7 @@ let observe_tac s tac g =
 let nf_zeta =
   Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     Environ.empty_env
-    Evd.empty
+    (Evd.from_env Environ.empty_env)
 
 let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ab03f1831..72bb8253d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -106,12 +106,12 @@ let const_of_ref = function
 
 let nf_zeta env =
   Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-    env
-    Evd.empty
+    env (Evd.from_env env)
 
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
+  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env
+    (Evd.from_env Environ.empty_env)
 
 
 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23..c21921513 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -613,10 +613,12 @@ END
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
  | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
-           [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
-             let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
-             let tc = EConstr.to_constr Evd.empty tc in
-             let tb = EConstr.to_constr Evd.empty tb in
+           [ let env = Global.env () in
+             let evd = Evd.from_env env in
+             let tc,_ctx = Constrintern.interp_constr env evd c in
+             let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
+             let tc = EConstr.to_constr evd tc in
+             let tb = EConstr.to_constr evd tb in
              Global.register f tc tb ]
 END
 
@@ -779,7 +781,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
-            let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in
+            let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
 	    change_concl c
           end;
 	  simplest_case a]
@@ -1106,7 +1108,9 @@ END
 VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
 | [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
   let get_key c =
-    let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+    let env = Global.env () in
+    let evd = Evd.from_env env in
+    let (evd, c) = Constrintern.interp_open_constr env evd c in
     let kind c = EConstr.kind evd c in
     Keys.constr_key kind c
   in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bd02d85d5..3dfe308a5 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) =
              let open Genprint in
              match generic_top_print (in_gen (Topwit wit) x) with
              | TopPrinterBasic pr -> pr ()
-             | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+             | TopPrinterNeedsContext pr ->
+               let env = Global.env() in
+               pr env (Evd.from_env env)
              | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
-                printer (Global.env()) Evd.empty default_ensure_surrounded
+               let env = Global.env() in
+               printer env (Evd.from_env env) default_ensure_surrounded
           end
         | _ -> default
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1b86583da..b91315aca 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m =
   let evd = solve_constraints env !evd in
   let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
-  Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
+  Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e455ebb28..3594c8765 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -369,8 +369,11 @@ let coq_True = lazy (init_constant "True")
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
 (* For unfold *)
-let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
-  | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+let evaluable_ref_of_constr s c =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  match EConstr.kind evd (Lazy.force c) with
+  | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 05dbf0a86..7ac9ea89d 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -377,7 +377,10 @@ let interp_head_pat hpat =
   | Cast (c', _, _) -> loop c'
   | Prod (_, _, c') -> loop c'
   | LetIn (_, _, _, c') -> loop c'
-  | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in
+  | _ ->
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
   filter_head, loop
 
 let all_true _ = true
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0dd3625ba..93c63d522 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -708,9 +708,9 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
 ;;
 
 
-let fixed_upat = function
+let fixed_upat evd = function
 | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false 
-| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
+| {up_t = t} -> not (occur_existential evd (EConstr.of_constr t)) (** FIXME *)
 
 let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
 
@@ -769,7 +769,7 @@ let mk_tpattern_matcher ?(all_instances=false)
 let p2t p = mkApp(p.up_f,p.up_a) in 
 let source () = match upats_origin, upats with
   | None, [p] -> 
-      (if fixed_upat p then str"term " else str"partial term ") ++ 
+      (if fixed_upat ise p then str"term " else str"partial term ") ++
       pr_constr_pat (p2t p) ++ spc()
   | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
       pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 779508477..fc398df9a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -929,9 +929,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
 let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
-      let ref',t = subst_global subst ref in
-	if ref' == ref then raw else
-         DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t))
+    let ref',t = subst_global subst ref in
+    if ref' == ref then raw else
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
 
   | GSort _
   | GVar _
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 40f4d4ff8..27b029aad 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -42,7 +42,7 @@ type recursion_scheme_error =
 
 exception RecursionSchemeError of recursion_scheme_error
 
-let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
 let name_assumption env = function
 | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
 | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 375ed10d0..9342b4cc7 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,9 +279,11 @@ let lift_pattern k = liftn_pattern k 1
 let rec subst_pattern subst pat =
   match pat with
   | PRef ref ->
-      let ref',t = subst_global subst ref in
-	if ref' == ref then pat else
-	 pattern_of_constr (Global.env()) Evd.empty t
+    let ref',t = subst_global subst ref in
+    if ref' == ref then pat else
+      let env = Global.env () in
+      let evd = Evd.from_env env in
+      pattern_of_constr env evd t
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 278a4761d..856894d9a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -165,7 +165,7 @@ let error_not_product ?loc env sigma c =
 (*s Error in conversion from AST to glob_constr *)
 
 let error_var_not_found ?loc s =
-  raise_pretype_error ?loc (empty_env, Evd.empty, VarNotFound s)
+  raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
 
 (*s Typeclass errors *)
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9eb410f06..56a883099 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -199,7 +199,7 @@ let warn_projection_no_head_constant =
           let env = Termops.push_rels_assum sign env in
           let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-          let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in
+          let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
           ++ term_pp ++ strbrk " in canonical instance "
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
@@ -211,7 +211,7 @@ let compute_canonical_projections warn (con,ind) =
   let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
   let c = Environ.constant_value_in env (con,u) in
-  let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+  let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
   let lt = List.rev_map snd sign in
@@ -317,7 +317,9 @@ let check_and_decompose_canonical_structure ref =
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref "Could not find its value in the global environment." in
-  let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
     | App (f,args) -> f,args
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index d036fec21..895181bc5 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -77,7 +77,9 @@ let print_ref reduce ref udecl =
   let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
-      let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
@@ -717,7 +719,10 @@ let print_eval x = !object_pr.print_eval x
 (**** Printing declarations and judgments *)
 (****  Abstract layer                 *****)
 
-let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x
+let print_typed_value x =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  print_typed_value_in_env env sigma x
 
 let print_judgment env sigma {uj_val=trm;uj_type=typ} =
   print_typed_value_in_env env sigma (trm, typ)
diff --git a/printing/printer.ml b/printing/printer.ml
index 88a1ab729..72030dc9f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -299,8 +299,8 @@ let pr_puniverses f env (c,u) =
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
 let pr_existential_key = Termops.pr_existential_key
 let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
-let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
-let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
+let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr)
 
 let pr_pconstant = pr_puniverses pr_constant
 let pr_pinductive = pr_puniverses pr_inductive
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 3c805b327..be8bc1357 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -323,7 +323,6 @@ let print_body is_impl env mp (l,body) =
 	 else Univ.Instance.empty
        in
        let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
-       let sigma = Evd.empty in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
 	| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -332,17 +331,17 @@ let print_body is_impl env mp (l,body) =
 	  | None -> mt ()
 	  | Some env ->
 	    str " :" ++ spc () ++
-	    hov 0 (Printer.pr_ltype_env env sigma
+            hov 0 (Printer.pr_ltype_env env (Evd.from_env env)
 		(Vars.subst_instance_constr u
    		  cb.const_type)) ++
 	    (match cb.const_body with
 	      | Def l when is_impl ->
 		spc () ++
 		hov 2 (str ":= " ++
-		       Printer.pr_lconstr_env env sigma
+                       Printer.pr_lconstr_env env (Evd.from_env env)
 			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx sigma ctx)
+            Printer.pr_universe_ctx (Evd.from_env env) ctx)
     | SFBmind mib ->
       try
 	let env = Option.get env in
@@ -387,7 +386,7 @@ let rec print_typ_expr env mp locals mty =
       let s = String.concat "." (List.map Id.to_string idl) in
       (* XXX: What should env and sigma be here? *)
       let env = Global.env () in
-      let sigma = Evd.empty in
+      let sigma = Evd.from_env env in
       hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
              ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
              ++ Printer.pr_lconstr_env env sigma c)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ea5d4719c..3e08c6d87 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1174,7 +1174,7 @@ let solve_inst env evd filter unique split fail =
 let _ =
   Hook.set Typeclasses.solve_all_instances_hook solve_inst
 
-let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
+let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 715686ad0..eede13329 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -78,7 +78,7 @@ let build_dependent_inductive ind (mib,mip) =
        Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt
        @ Context.Rel.to_extended_list mkRel 0 realargs)
 
-let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na
 let name_assumption env = function
 | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
 | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
@@ -109,7 +109,7 @@ let get_coq_eq ctx =
 
 let univ_of_eq env eq =
   let eq = EConstr.of_constr eq in
-  match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with
+  match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with
   | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
   | _ -> assert false
 
@@ -620,7 +620,9 @@ let build_r2l_forward_rew_scheme dep env ind kind =
 (**********************************************************************)
 
 let fix_r2l_forward_rew_scheme (c, ctx') =
-  let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let t = EConstr.Unsafe.to_constr t in
   let ctx,_ = decompose_prod_assum t in
   match ctx with
@@ -630,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
         (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
 	  (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
 	    (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
-	      (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty
+              (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
 		(EConstr.of_constr (applist (c,
 	          Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
       in c', ctx'
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3ade5314b..786760122 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1263,7 +1263,9 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
   let c' = iter c in
-    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
+    let env = Global.env () in
+    let empty_sigma = Evd.from_env env in
+    if check then Pretyping.check_evars env empty_sigma sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
@@ -1276,7 +1278,9 @@ let interp_hints poly =
   let sigma = Evd.from_env env in
   let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
-      prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+      prepare_hint true (poly,false) env sigma (evd,c) in
   let fref r =
     let gr = global_with_alias r in
     Dumpglob.add_glob ?loc:r.CAst.loc gr;
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 412954989..b346ed223 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -292,7 +292,7 @@ let error_too_many_names pats =
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
     str ": " ++ pr_enum (Miscprint.pr_intro_pattern
-                           (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+                           (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++
     str ".")
 
 let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
@@ -496,9 +496,10 @@ let wrap_inv_error id = function (e, info) -> match e with
   | Indrec.RecursionSchemeError
       (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
       Proofview.tclENV >>= fun env ->
+      Proofview.tclEVARMAP >>= fun sigma ->
       tclZEROMSG (
 	(strbrk "Inversion would require case analysis on sort " ++
-	pr_sort Evd.empty k ++
+        pr_sort sigma k ++
 	strbrk " which is not allowed for inductive definition " ++
 	pr_inductive env (fst i) ++ str "."))
   | e -> Proofview.tclZERO ~info e
diff --git a/vernac/class.ml b/vernac/class.ml
index 06e1694f9..133726702 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -67,7 +67,7 @@ let explain_coercion_error g = function
 let check_reference_arity ref =
   let env = Global.env () in
   let c, _ = Global.type_of_global_in_context env ref in
-  if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then
+  if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then
     raise (CoercionError (NotAClass ref))
 
 let check_arity = function
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 61ce5d6c4..d99d45313 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -196,7 +196,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	let (_, ty_constr) = instance_constructor (k,u) subst in
         let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
         let sigma = Evd.minimize_universes sigma in
-        Pretyping.check_evars env Evd.empty sigma termtype;
+        Pretyping.check_evars env (Evd.from_env env) sigma termtype;
         let univs = Evd.check_univ_decl ~poly sigma decl in
         let termtype = to_constr sigma termtype in
         let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
@@ -290,7 +290,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
       (* Beware of this step, it is required as to minimize universes. *)
       let sigma = Evd.minimize_universes sigma in
       (* Check that the type is free of evars now. *)
-      Pretyping.check_evars env Evd.empty sigma termtype;
+      Pretyping.check_evars env (Evd.from_env env) sigma termtype;
       let termtype = to_constr sigma termtype in
       let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
         if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
@@ -365,7 +365,7 @@ let context poly l =
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in
   (* Note, we must use the normalized evar from now on! *)
   let sigma = Evd.minimize_universes sigma in
-  let ce t = Pretyping.check_evars env Evd.empty sigma t in
+  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 722f21171..492ae1d9b 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -157,7 +157,7 @@ let do_assumptions kind nl l =
       ((sigma,env,ienv),((is_coe,idl),t,imps)))
     (sigma,env,empty_internalization_env) l
   in
-  let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in
+  let sigma = solve_remaining_evars all_and_fail_flags env sigma (Evd.from_env env) in
   (* The universe constraints come from the whole telescope. *)
   let sigma = Evd.minimize_universes sigma in
   let nf_evar c = EConstr.to_constr sigma c in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 863adb0d1..2d4bd6779 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,7 +104,9 @@ let interp_definition pl bl poly red_option c ctypopt =
   (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;
+  let env = Global.env () in
+  let empty_sigma = Evd.from_env env in
+  check_evars_are_solved env evd empty_sigma;
   ce
 
 let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 85c0699ea..d996443d6 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -232,7 +232,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   (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;
+  check_evars_are_solved env evd (Evd.from_env env);
   if List.for_all Option.has_some fixdefs then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env evd isfix (List.combine fixnames fixdefs)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 629fcce5a..790e83dbe 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,7 +367,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
      () in
 
   (* Try further to solve evars, and instantiate them *)
-  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
+  let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
@@ -381,10 +381,10 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   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 c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+  Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
-    List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps)
+    List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
     constructors;
 
   (* Build the inductive entries *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 1add1f486..d4c5def6f 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -848,9 +848,9 @@ let explain_not_match_error = function
     str "the body of definitions differs"
   | NotConvertibleTypeField (env, typ1, typ2) ->
     str "expected type" ++ spc ()  ++
-    quote (Printer.safe_pr_lconstr_env env Evd.empty typ2) ++ spc () ++
+    quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ2) ++ spc () ++
     str "but found type" ++ spc () ++
-    quote (Printer.safe_pr_lconstr_env env Evd.empty typ1)
+    quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ1)
   | NotSameConstructorNamesField ->
     str "constructor names differ"
   | NotSameInductiveNameInBlockField ->
@@ -889,9 +889,9 @@ let explain_not_match_error = function
       Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
   | IncompatiblePolymorphism (env, t1, t2) ->
     str "conversion of polymorphic values generates additional constraints: " ++
-      quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
+      quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
       str "compared to " ++ spc () ++
-      quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
+      quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
       let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
@@ -1011,8 +1011,9 @@ let explain_module_internalization_error = function
 (* Typeclass errors *)
 
 let explain_not_a_class env c =
-  let c = EConstr.to_constr Evd.empty c in
-  pr_constr_env env Evd.empty c ++ str" is not a declared type class."
+  let sigma = Evd.from_env env in
+  let c = EConstr.to_constr sigma c in
+  pr_constr_env env sigma c ++ str" is not a declared type class."
 
 let explain_unbound_method env cid { CAst.v = id } =
   str "Unbound method name " ++ Id.print (id) ++ spc () ++
@@ -1025,7 +1026,7 @@ let pr_constr_exprs exprs =
 
 let explain_mismatched_contexts env c i j =
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
-    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env Evd.empty j) ++
+    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++
     fnl () ++ brk (1,1) ++
     hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
 
@@ -1087,19 +1088,19 @@ let explain_refiner_error env sigma = function
 (* Inductive errors *)
 
 let error_non_strictly_positive env c v =
-  let pc = pr_lconstr_env env Evd.empty c in
-  let pv = pr_lconstr_env env Evd.empty v in
+  let pc = pr_lconstr_env env (Evd.from_env env) c in
+  let pv = pr_lconstr_env env (Evd.from_env env) v in
   str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
   brk(1,1) ++ pc ++ str "."
 
 let error_ill_formed_inductive env c v =
-  let pc = pr_lconstr_env env Evd.empty c in
-  let pv = pr_lconstr_env env Evd.empty v in
+  let pc = pr_lconstr_env env (Evd.from_env env) c in
+  let pv = pr_lconstr_env env (Evd.from_env env) v in
   str "Not enough arguments applied to the " ++ pv ++
   str " in" ++ brk(1,1) ++ pc ++ str "."
 
 let error_ill_formed_constructor env id c v nparams nargs =
-  let pv = pr_lconstr_env env Evd.empty v in
+  let pv = pr_lconstr_env env (Evd.from_env env) v in
   let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
   str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++
   str "is not valid;" ++ brk(1,1) ++
@@ -1119,12 +1120,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
 
 let pr_ltype_using_barendregt_convention_env env c =
   (* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
-  quote (pr_goal_concl_style_env env Evd.empty (EConstr.of_constr c))
+  quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c))
 
 let error_bad_ind_parameters env c n v1 v2  =
   let pc = pr_ltype_using_barendregt_convention_env env c in
-  let pv1 = pr_lconstr_env env Evd.empty v1 in
-  let pv2 = pr_lconstr_env env Evd.empty v2 in
+  let pv1 = pr_lconstr_env env (Evd.from_env env) v1 in
+  let pv2 = pr_lconstr_env env (Evd.from_env env) v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
   str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
 
@@ -1142,7 +1143,7 @@ let error_same_names_overlap idl =
   prlist_with_sep pr_comma Id.print idl ++ str "."
 
 let error_not_an_arity env c =
-  str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++
+  str "The type" ++ spc () ++ pr_lconstr_env env (Evd.from_env env) c ++ spc () ++
   str "is not an arity."
 
 let error_bad_entry () =
@@ -1316,4 +1317,4 @@ let explain_reduction_tactic_error = function
       str "The abstracted term" ++ spc () ++
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
-      explain_type_error env' Evd.empty e
+      explain_type_error env' (Evd.from_env env') e
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 3bf0ca0a8..dfc51a990 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -266,7 +266,9 @@ let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
-  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty (EConstr.of_constr c))
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))
 
 exception NoObligations of Id.t option
 
@@ -521,8 +523,10 @@ let declare_mutual_definition l =
     List.split3
       (List.map (fun x -> 
 	let subs, typ = (subst_body true x) in
-	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len (EConstr.of_constr subs)) in
-	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len (EConstr.of_constr typ)) in
+        let env = Global.env () in
+        let sigma = Evd.from_env env in
+        let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
+        let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
 	let term = EConstr.Unsafe.to_constr term in
 	let typ = EConstr.Unsafe.to_constr typ in
 	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
@@ -1069,9 +1073,11 @@ let show_obligations_of_prg ?(msg=true) prg =
 		       if !showed > 0 then (
 		         decr showed;
 			 let x = subst_deps_obl obls x in
+                         let env = Global.env () in
+                         let sigma = Evd.from_env env in
 			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
 				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
-				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
+                                   hov 1 (Printer.pr_constr_env env sigma x.obl_type ++
 					    str "." ++ fnl ())))
 		   | Some _ -> ())
       obls
@@ -1087,9 +1093,11 @@ let show_obligations ?(msg=true) n =
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
     (Id.print n ++ spc () ++ str":" ++ spc () ++
-	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
-	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
+             Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+            ++ Printer.pr_constr_env env sigma prg.prg_body)
 
 let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
                    ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
diff --git a/vernac/record.ml b/vernac/record.ml
index bf6affd5f..5ff118473 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -152,7 +152,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
     interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
   in
   let sigma =
-    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in
+    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma (Evd.from_env env_ar) in
   let sigma, typ =
     let _, univ = compute_constructor_level sigma env_ar newfs in
       if not def && (Sorts.is_prop sort ||
@@ -172,7 +172,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   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 ce t = Pretyping.check_evars env0 (Evd.from_env env0) 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);
diff --git a/vernac/search.ml b/vernac/search.ml
index 6d07187fe..e8ccec11c 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -215,7 +215,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
 
 let search_about_filter query gr env typ = match query with
 | GlobSearchSubPattern pat ->
-  Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat (EConstr.of_constr typ)
+  Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ)
 | GlobSearchString s ->
   String.string_contains ~where:(name_of_reference gr) ~what:s
 
@@ -226,7 +226,7 @@ let search_pattern gopt pat mods pr_search =
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     module_filter mods ref env typ &&
-    pattern_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) &&
+    pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
     blacklist_filter ref env typ
   in
   let iter ref env typ =
@@ -250,8 +250,8 @@ let search_rewrite gopt pat mods pr_search =
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     module_filter mods ref env typ &&
-    (pattern_filter pat1 ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) ||
-       pattern_filter pat2 ref env Evd.empty (EConstr.of_constr typ)) &&
+    (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) ||
+       pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) &&
     blacklist_filter ref env typ
   in
   let iter ref env typ =
@@ -265,7 +265,7 @@ let search_by_head gopt pat mods pr_search =
   let blacklist_filter = blacklist_filter_aux () in
   let filter ref env typ =
     module_filter mods ref env typ &&
-    head_filter pat ref env Evd.empty (* FIXME *) (EConstr.of_constr typ) &&
+    head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) &&
     blacklist_filter ref env typ
   in
   let iter ref env typ =
@@ -329,12 +329,12 @@ let interface_search =
       toggle (Str.string_match regexp id 0) flag
     in
     let match_type (pat, flag) =
-      toggle (Constr_matching.is_matching env Evd.empty pat (EConstr.of_constr constr)) flag
+      toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
     in
     let match_subtype (pat, flag) =
       toggle
         (Constr_matching.is_matching_appsubterm ~closed:false 
-	   env Evd.empty pat (EConstr.of_constr constr)) flag
+           env (Evd.from_env env) pat (EConstr.of_constr constr)) flag
     in
     let match_module (mdl, flag) =
       toggle (Libnames.is_dirpath_prefix_of mdl path) flag
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1ce4e194..f347798c6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1651,7 +1651,9 @@ let vernac_check_may_eval ~atts redexp glopt rc =
 
 let vernac_declare_reduction ~atts s r =
   let local = make_locality atts.locality in
-  declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =