Merge PR #8974: Fix mod_subst wrt universe polymorphism

2 files changed, 12 insertions, 12 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index 9aca7788d2..db2e8bfaed 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -31,8 +31,8 @@ let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destCon
 
 let subst_constructor subst (ind,j as ref) =
   let ind' = subst_ind subst ind in
-    if ind==ind' then ref, mkConstruct ref
-    else (ind',j), mkConstruct (ind',j)
+  if ind==ind' then ref
+  else (ind',j)
 
 let subst_global_reference subst ref = match ref with
   | VarRef var -> ref
@@ -43,20 +43,20 @@ let subst_global_reference subst ref = match ref with
     let ind' = subst_ind subst ind in
       if ind==ind' then ref else IndRef ind'
   | ConstructRef ((kn,i),j as c) ->
-    let c',t = subst_constructor subst c in
-      if c'==c then ref else ConstructRef c'
+    let c' = subst_constructor subst c in
+    if c'==c then ref else ConstructRef c'
 
 let subst_global subst ref = match ref with
-  | VarRef var -> ref, mkVar var
+  | VarRef var -> ref, None
   | ConstRef kn ->
-     let kn',t = subst_con_kn subst kn in
-      if kn==kn' then ref, mkConst kn else ConstRef kn', t
+     let kn',t = subst_con subst kn in
+      if kn==kn' then ref, None else ConstRef kn', t
   | IndRef ind ->
       let ind' = subst_ind subst ind in
-      if ind==ind' then ref, mkInd ind else IndRef ind', mkInd ind'
+      if ind==ind' then ref, None else IndRef ind', None
   | ConstructRef ((kn,i),j as c) ->
-      let c',t = subst_constructor subst c in
-	if c'==c then ref,t else ConstructRef c', t
+      let c' = subst_constructor subst c in
+      if c'==c then ref,None else ConstructRef c', None
 
 let canonical_gr = function
   | ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con))
diff --git a/library/globnames.mli b/library/globnames.mli
index a96a42ced2..d49ed453f5 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -36,8 +36,8 @@ val destConstructRef : GlobRef.t -> constructor
 
 val is_global : GlobRef.t -> constr -> bool
 
-val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
+val subst_constructor : substitution -> constructor -> constructor
+val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
 (** This constr is not safe to be typechecked, universe polymorphism is not