Merge PR #8866: Check universe instances in Typing

4 files changed, 16 insertions, 37 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e341412294..f61dd0c101 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -350,9 +350,6 @@ let map_universes f env =
     { env with env_stratification =
 	 { s with env_universes = f s.env_universes } }
 
-let set_universes env u =
-  { env with env_stratification = { env.env_stratification with env_universes = u } }
-
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
   else map_universes (UGraph.merge_constraints c) env
@@ -405,19 +402,12 @@ let add_constant_key kn cb linkinfo env =
 let add_constant kn cb env =
   add_constant_key kn cb no_link_info env
 
-let constraints_of cb u =
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
-
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
-  | Polymorphic_const _ctx ->
-    let csts = constraints_of cb u in
-    (subst_instance_constr u cb.const_type, csts)
+  let uctx = Declareops.constant_polymorphic_context cb in
+  let csts = Univ.AUContext.instantiate u uctx in
+  (subst_instance_constr u cb.const_type, csts)
 
 type const_evaluation_result = NoBody | Opaque
 
@@ -425,20 +415,14 @@ exception NotEvaluableConst of const_evaluation_result
 
 let constant_value_and_type env (kn, u) =
   let cb = lookup_constant kn env in
-    if Declareops.constant_is_polymorphic cb then
-      let cst = constraints_of cb u in
-      let b' = match cb.const_body with
-	| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
-	| OpaqueDef _ -> None
-	| Undef _ -> None
-      in
-	b', subst_instance_constr u cb.const_type, cst
-    else 
-      let b' = match cb.const_body with
-	| Def l_body -> Some (Mod_subst.force_constr l_body)
-	| OpaqueDef _ -> None
-	| Undef _ -> None
-      in b', cb.const_type, Univ.Constraint.empty
+  let uctx = Declareops.constant_polymorphic_context cb in
+  let cst = Univ.AUContext.instantiate u uctx in
+  let b' = match cb.const_body with
+    | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
+    | OpaqueDef _ -> None
+    | Undef _ -> None
+  in
+  b', subst_instance_constr u cb.const_type, cst
 
 let body_of_constant_body env cb =
   let otab = opaque_tables env in
@@ -457,9 +441,7 @@ let body_of_constant_body env cb =
 (* constant_type gives the type of a constant *)
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
-    if Declareops.constant_is_polymorphic cb then
-      subst_instance_constr u cb.const_type
-    else cb.const_type
+  subst_instance_constr u cb.const_type
 
 let constant_value_in env (kn,u) =
   let cb = lookup_constant kn env in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0255581749..c285f907fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -155,11 +155,6 @@ val named_body : variable -> env -> constr option
 val fold_named_context :
   (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-val set_universes : env -> UGraph.t -> env
-(** This is used to update universes during a proof for the sake of
-   evar map-unaware functions, eg [Typing] calling
-   [Typeops.check_hyps_inclusion]. *)
-
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1bb2d3c79c..c8fd83c8a9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -91,7 +91,8 @@ let type_of_variable env id =
 (* Checks if a context of variables can be instantiated by the
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env f c sign =
+let check_hyps_inclusion env ?evars f c sign =
+  let conv env a b = conv env ?evars a b in
   Context.Named.fold_outside
     (fun d1 () ->
       let open Context.Named.Declaration in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d24002065b..4193324136 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -116,4 +116,5 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
+val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+  ('a -> constr) -> 'a -> Constr.named_context -> unit