Correct coqchk checking subtyping relation for inductives

3 files changed, 5 insertions, 24 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 00ff447cc..69dd6f57a 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -551,10 +551,10 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 let check_subtyping mib paramsctxt env_ar inds =
     let numparams = rel_context_nhyps paramsctxt in
     let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
-    let dosubst = subst_univs_level_constr sbsubst in
+    let dosubst = subst_instance_constr sbsubst in
     let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
-    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in
     let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
     let env' = Environ.push_context uctx env_ar in
     let env'' = Environ.push_context uctx_other env' in
diff --git a/checker/univ.ml b/checker/univ.ml
index fa884d9d0..525f535e9 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1194,8 +1194,7 @@ struct
                              create_trivial_subtyping inst freshunivs))
 
   let subtyping_susbst (univcst, subtypcst) =
-      let (ctx, ctx') = (halve_context (UContext.instance subtypcst)) in
-      Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
+      let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
 
 end
 
@@ -1232,22 +1231,6 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
-let subst_univs_level_instance subst i =
-  let i' = Instance.subst_fn (subst_univs_level_level subst) i in
-    if i == i' then i
-    else i'
-
-let subst_univs_level_constraint subst (u,d,v) =
-  let u' = subst_univs_level_level subst u 
-  and v' = subst_univs_level_level subst v in
-    if d != Lt && Level.equal u' v' then None
-    else Some (u',d,v')
-
-let subst_univs_level_constraints subst csts =
-  Constraint.fold 
-    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
-    csts Constraint.empty 
-
 (** Substitute instance inst for ctx in csts *)
 
 let subst_instance_level s l =
diff --git a/checker/univ.mli b/checker/univ.mli
index edf828dae..2bc2653e0 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -213,7 +213,7 @@ sig
 
   val from_universe_context : universe_context -> universe_instance -> t
 
-  val subtyping_susbst : t -> universe_level_subst
+  val subtyping_susbst : t -> universe_instance
 
 end
 
@@ -238,8 +238,6 @@ val is_empty_level_subst : universe_level_subst -> bool
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
-val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
-val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 
 (** Level to universe substitutions. *)