diff options
author | 2018-05-28 13:38:23 +0200 | |
---|---|---|
committer | 2018-05-28 13:38:23 +0200 | |
commit | 81535edc4b21015bd63d23e57ca9d707b4b71f6b (patch) | |
tree | 6a76bc46b66cade1b53d2c878ae2aa7c5e1f5dc5 /printing/prettyp.ml | |
parent | b2f746e41abf53fc481f90804ba4d70edd73fc86 (diff) | |
parent | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (diff) |
Merge PR #7419: Remove 100 occurrences of Evd.empty
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r-- | printing/prettyp.ml | 9 |
1 files changed, 7 insertions, 2 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) |