From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- printing/printer.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index e014baa2cd..a3d0eaac2e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -121,6 +121,7 @@ val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -- cgit v1.2.3 From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- printing/printer.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index a3d0eaac2e..67128da407 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -122,6 +122,7 @@ val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t +val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -- cgit v1.2.3