diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | library/global.mli | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/library/global.ml b/library/global.ml index 0fc9e11364..6bb4614aa4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -119,6 +119,7 @@ let add_module_parameter mbid mte inl = (** Queries on the global environment *) let universes () = universes (env()) +let universes_lbound () = universes_lbound (env()) let named_context () = named_context (env()) let named_context_val () = named_context_val (env()) @@ -181,6 +182,10 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r +let is_template_checked r = is_template_checked (env ()) r + +let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r + let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = diff --git a/library/global.mli b/library/global.mli index b089b7dd80..d0bd556d70 100644 --- a/library/global.mli +++ b/library/global.mli @@ -22,6 +22,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool val universes : unit -> UGraph.t +val universes_lbound : unit -> Univ.Level.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Constr.named_context @@ -136,6 +137,8 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool +val is_template_checked : GlobRef.t -> bool +val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool (** {6 Retroknowledge } *) |