Merge PR #9317: Restrict universes in records.

Ack-by: SkySkimmer
Reviewed-by: mattam82
Reviewed-by: ppedrot

4 files changed, 25 insertions, 9 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 3d98381fbb..1cc6e79485 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -134,6 +134,15 @@ struct
           let ty' = f ty in
           if v == v' && ty == ty' then decl else LocalDef (na, v', ty')
 
+    let map_constr_het f = function
+      | LocalAssum (na, ty) ->
+          let ty' = f ty in
+          LocalAssum (na, ty')
+      | LocalDef (na, v, ty) ->
+          let v' = f v in
+          let ty' = f ty in
+          LocalDef (na, v', ty')
+
     (** Perform a given action on all terms in a given declaration. *)
     let iter_constr f = function
       | LocalAssum (_,ty) -> f ty
diff --git a/kernel/context.mli b/kernel/context.mli
index 2b0d36cb8c..8acae73680 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -78,6 +78,9 @@ sig
     (** Map all terms in a given declaration. *)
     val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
 
+    (** Map all terms, with an heterogeneous function. *)
+    val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt
+
     (** Perform a given action on all terms in a given declaration. *)
     val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
 
diff --git a/test-suite/bugs/closed/bug_8076.v b/test-suite/bugs/closed/bug_8076.v
new file mode 100644
index 0000000000..7bee43620f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8076.v
@@ -0,0 +1,3 @@
+
+Notation leak a := ltac:(let x := constr:(Type) in exact a) (only parsing).
+Record foo@{} (P:leak Prop) := { f : leak Prop }.
diff --git a/vernac/record.ml b/vernac/record.ml
index 8032a6a04c..1b7b828f47 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -176,19 +176,20 @@ let typecheck_params_and_fields finite def poly pl ps records =
         else sigma, typ
   in
   let (sigma, typs) = List.fold_left2_map fold sigma typs data in
-  let sigma = Evd.minimize_universes sigma in
-  let newps = List.map (EConstr.to_rel_decl sigma) newps in
+  let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf ->
+      let newps = List.map (RelDecl.map_constr_het nf) newps in
+      let map (impls, newfs) typ =
+        let newfs = List.map (RelDecl.map_constr_het nf) newfs in
+        let typ = nf typ in
+        (typ, impls, newfs)
+      in
+      let ans = List.map2 map data typs in
+      newps, ans)
+  in
   let univs = Evd.check_univ_decl ~poly sigma decl in
   let ubinders = Evd.universe_binders sigma in
   let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
   let () = List.iter (iter_constr ce) (List.rev newps) in
-  let map (impls, newfs) typ =
-    let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
-    let typ = EConstr.to_constr sigma typ in
-    List.iter (iter_constr ce) (List.rev newfs);
-    (typ, impls, newfs)
-  in
-  let ans = List.map2 map data typs in
   ubinders, univs, template, newps, imps, ans
 
 type record_error =