aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml9
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printmod.ml9
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)