Remove some occurrences of Evd.empty

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

4 files changed, 16 insertions, 9 deletions

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