diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 11 |
1 files changed, 10 insertions, 1 deletions
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 *) |