diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-13 19:38:13 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
commit | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (patch) | |
tree | 21bda11bb7526d8dccc8c3883245ecf02762fc74 | |
parent | 575da16f72ac125ba7e50b1bfe63302dee639973 (diff) |
Print the type-in-type flag in various user-facing functions.
-rw-r--r-- | printing/prettyp.ml | 7 | ||||
-rw-r--r-- | toplevel/assumptions.ml | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9745a7925..ad67becd0 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -215,6 +215,12 @@ let print_polymorphism ref = else "not universe polymorphic") ] else [] +let print_type_in_type ref = + let unsafe = Global.is_type_in_type ref in + if unsafe then + [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] + else [] + let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with @@ -244,6 +250,7 @@ let print_name_infos ref = else [] in print_polymorphism ref @ + print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ print_renames_list (mt()) renames @ diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index c05c5f6c2..921c4a1d8 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -293,7 +293,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try Refmap_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu in - if not (Declareops.constant_has_body cb) then + if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then let t = type_of_constant cb in let l = try Refmap_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu |