diff options
| author | Matthieu Sozeau | 2014-03-25 18:29:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | 62fb849cf9410ddc2d9f355570f4fb859f3044c3 (patch) | |
| tree | 2f350ca302a46e18840638d20e7ff89beaf2b1f0 /printing | |
| parent | ca318cd0d21ce157a3042b600ded99df6face25e (diff) | |
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 87d7e0980d..e36019887d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -378,17 +378,18 @@ let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Declareops.body_of_constant cb in let typ = ungeneralized_type_of_constant_type cb.const_type in + let univs = Declareops.universes_of_constant cb in hov 0 (pr_polymorphic cb.const_polymorphic ++ match val_0 with | None -> str"*** [ " ++ print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_universe_ctx (Future.force cb.const_universes) + Printer.pr_universe_ctx univs | _ -> print_basename sp ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_universe_ctx (Future.force cb.const_universes)) + Printer.pr_universe_ctx univs) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ |