Remove some occurrences of Evd.empty

We address the easy ones, but they should probably be all removed.

11 files changed, 57 insertions, 44 deletions

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 =