diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 02e59a227..67ca1b666 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -252,7 +252,8 @@ let print_namespace ns = print_list pr_id qn in let print_constant k body = - let t = body.Declarations.const_type in + (* FIXME: universes *) + let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in print_kn k ++ str":" ++ spc() ++ Printer.pr_type t in let matches mp = match match_modulepath ns mp with |