diff options
| author | Pierre-Marie Pédrot | 2016-11-26 16:18:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:44 +0100 |
| commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
| tree | fc84ec244390beb2f495b024620af2e130ad5852 /printing/prettyp.ml | |
| parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) | |
Definining EConstr-based contexts.
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 93970512da..64c7c0ba5e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,11 +71,11 @@ let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = let typ = Global.type_of_global_unsafe ref in + let typ = EConstr.of_constr typ in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty (EConstr.of_constr typ) in - let ccl = EConstr.Unsafe.to_constr ccl - in Term.it_mkProd_or_LetIn ccl ctx + let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in let env = Global.env () in @@ -85,7 +85,7 @@ let print_ref reduce ref = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () in - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ Printer.pr_universe_ctx sigma univs) (********************************) |