Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

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 } *)