Merge PR #9317: Restrict universes in records.

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

2 files changed, 12 insertions, 0 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