From a9240de59f6822f55a57d0e6453bd0635795720d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 11 Nov 2017 22:02:20 +0100 Subject: Print inductive cumulativity info in About. --- printing/prettyp.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'printing/prettyp.ml') diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 2b7886d11..114a071ee 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -78,6 +78,15 @@ let print_ref reduce ref udecl = in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let variance = match ref with + | VarRef _ | ConstRef _ -> None + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> + let mind = Environ.lookup_mind ind (Global.env ()) in + begin match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None + | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) + end + in let inst = Univ.AUContext.instance univs in let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in @@ -89,7 +98,7 @@ let print_ref reduce ref udecl = else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_universe_ctx sigma univs) + Printer.pr_universe_ctx sigma ?variance univs) (********************************) (** Printing implicit arguments *) -- cgit v1.2.3