Fix mod_subst wrt universe polymorphism

5 files changed, 32 insertions, 22 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f18040accb..306a76e35e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -192,9 +192,11 @@ let subst_cl_typ subst ct = match ct with
     let c' = subst_proj_repr subst c in
       if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
-      let c',t = subst_con_kn subst c in
-	if c' == c then ct else
-         pi1 (find_class_type Evd.empty (EConstr.of_constr t))
+      let c',t = subst_con subst c in
+      if c' == c then ct else (match t with
+          | None -> CL_CONST c'
+          | Some t ->
+            pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
   | CL_IND i ->
       let i' = subst_ind subst i in
 	if i' == i then ct else CL_IND i'
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33ced6d6e0..bcfa2df56b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -933,10 +933,13 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
     let ref',t = subst_global subst ref in
-    if ref' == ref then raw else
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
+    if ref' == ref then raw else (match t with
+        | None -> GRef (ref', u)
+        | Some t ->
+          let env = Global.env () in
+          let evd = Evd.from_env env in
+          let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *)
+          DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)))
 
   | GSort _
   | GVar _
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index e533930267..ccbb2934bc 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -147,13 +147,16 @@ let cache_head o =
 
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
-      let cst,c = subst_con_kn subst cst in
-      if isConst c && Constant.equal (fst (destConst c)) cst then
-        (* A change of the prefix of the constant *)
-        k
-      else
-        (* A substitution of the constant by a functor argument *)
-        kind_of_head (Global.env()) c
+    let cst',c = subst_con subst cst in
+    if cst == cst' then k
+    else
+      (match c with
+       | None ->
+         (* A change of the prefix of the constant *)
+         RigidHead (RigidParameter cst')
+       | Some c ->
+         (* A substitution of the constant by a functor argument *)
+         kind_of_head (Global.env()) c.Univ.univ_abstracted_value)
   | x -> x
 
 let subst_head (subst,(ref,k)) =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3c1c470053..9c93f29e06 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,10 +279,12 @@ let rec subst_pattern subst pat =
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
-    if ref' == ref then pat else
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      pattern_of_constr env evd t
+    if ref' == ref then pat else (match t with
+        | None -> PRef ref'
+        | Some t ->
+          let env = Global.env () in
+          let evd = Evd.from_env env in
+          pattern_of_constr env evd t.Univ.univ_abstracted_value)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fe9b69dbbc..bc35bedd2c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -71,12 +71,12 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
    List.Smart.map
-     (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn)))
+     (Option.Smart.map (subst_constant subst))
     projs
   in
-  let id' = fst (subst_constructor subst id) in
-    if projs' == projs && kn' == kn && id' == id then obj else
-      ((kn',i),id',kl,projs')
+  let id' = subst_constructor subst id in
+  if projs' == projs && kn' == kn && id' == id then obj else
+    ((kn',i),id',kl,projs')
 
 let discharge_structure (_,x) = Some x