From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 3 May 2018 17:44:34 +0200 Subject: Remove some occurrences of Evd.empty We address the easy ones, but they should probably be all removed. --- printing/prettyp.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'printing/prettyp.ml') 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) -- cgit v1.2.3