Remove some occurrences of Evd.empty

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

3 files changed, 13 insertions, 9 deletions

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 77466605a..23c81cfcb 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)