Merge PR #8974: Fix mod_subst wrt universe polymorphism

1 files changed, 9 insertions, 0 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7b5ed05bda..93a91af1d7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -978,6 +978,15 @@ struct
 
 end
 
+type 'a univ_abstracted = {
+  univ_abstracted_value : 'a;
+  univ_abstracted_binder : AUContext.t;
+}
+
+let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
+  let univ_abstracted_value = f univ_abstracted_value in
+  {univ_abstracted_value;univ_abstracted_binder}
+
 let hcons_abstract_universe_context = AUContext.hcons
 
 (** Universe info for cumulative inductive types: A context of