6 files changed, 106 insertions, 4 deletions

diff --git a/engine/universes.ml b/engine/universes.ml
index 194de2cee..f2942be6d 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -32,9 +32,37 @@ let universe_binders_of_global ref : universe_binders =
     let l = Refmap.find ref !universe_binders_table in l
   with Not_found -> Names.Id.Map.empty
 
-let register_universe_binders ref l =
+let cache_ubinder (_,(ref,l)) =
   universe_binders_table := Refmap.add ref l !universe_binders_table
 
+let subst_ubinder (subst,(ref,l as orig)) =
+  let ref' = fst (Globnames.subst_global subst ref) in
+  if ref == ref' then orig else ref', l
+
+let discharge_ubinder (_,(ref,l)) =
+  Some (Lib.discharge_global ref, l)
+
+let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj =
+  let open Libobject in
+  declare_object { (default_object "universe binder") with
+    cache_function = cache_ubinder;
+    load_function = (fun _ x -> cache_ubinder x);
+    classify_function = (fun x -> Substitute x);
+    subst_function = subst_ubinder;
+    discharge_function = discharge_ubinder;
+    rebuild_function = (fun x -> x); }
+
+let register_universe_binders ref ubinders =
+  (* Add the polymorphic (section) universes *)
+  let open Names in
+  let ubinders = Idmap.fold (fun id (poly,lvl) ubinders ->
+      if poly then Id.Map.add id lvl ubinders
+      else ubinders)
+      (fst (Global.global_universe_names ())) ubinders
+  in
+  if not (Id.Map.is_empty ubinders)
+  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+
 type univ_name_list = Name.t Loc.located list
 
 let universe_binders_with_opt_names ref levels = function
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f169f86e8..6865dcc76 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -95,7 +95,8 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
-  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log \
+  prerequisite/bind_univs.v.log
 
 #######################################################################
 # Phony targets
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 6fb8cba18..04bd169bd 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -84,3 +84,44 @@ The command has indeed failed with message:
 Universe instance should have length 0
 The command has indeed failed with message:
 This object does not support universe names.
+Monomorphic bind_univs.mono = Type@{u}
+     : Type@{u+1}
+(* {u} |=  *)
+
+bind_univs.mono is not universe polymorphic
+bind_univs.poly@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+bind_univs.poly is universe polymorphic
+insec@{v} = Type@{u} -> Type@{v}
+     : Type@{max(u+1, v+1)}
+(* v |=  *)
+
+insec is universe polymorphic
+insec@{u v} = Type@{u} -> Type@{v}
+     : Type@{max(u+1, v+1)}
+(* u v |=  *)
+
+insec is universe polymorphic
+inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+inmod is universe polymorphic
+SomeMod.inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+SomeMod.inmod is universe polymorphic
+inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+inmod is universe polymorphic
+Applied.infunct@{u v} = 
+inmod@{u} -> Type@{v}
+     : Type@{max(u+1, v+1)}
+(* u v |=  *)
+
+Applied.infunct is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 46904b384..f0a990986 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -52,3 +52,30 @@ Fail Print mono@{E}.
 
 (* Not everything can be printed with custom universe names. *)
 Fail Print Coq.Init.Logic@{E}.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.
+
+Section SomeSec.
+  Universe u.
+  Definition insec@{v} := Type@{u} -> Type@{v}.
+  Print insec.
+End SomeSec.
+Print insec.
+
+Module SomeMod.
+  Definition inmod@{u} := Type@{u}.
+  Print inmod.
+End SomeMod.
+Print SomeMod.inmod.
+Import SomeMod.
+Print inmod.
+
+Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
+Module SomeFunct (In : SomeTyp).
+  Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+End SomeFunct.
+Module Applied := SomeFunct(SomeMod).
+Print Applied.infunct.
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
new file mode 100644
index 000000000..f17c00e9d
--- /dev/null
+++ b/test-suite/prerequisite/bind_univs.v
@@ -0,0 +1,5 @@
+(* Used in output/UnivBinders.v *)
+
+Monomorphic Definition mono@{u} := Type@{u}.
+
+Polymorphic Definition poly@{u} := Type@{u}.
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a787ec6fa..42631a15b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           (locality, ConstRef kn)
     in
     definition_message id;
-    Option.iter (Universes.register_universe_binders r) pl;
+    Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
     call_hook (fun exn -> exn) hook l r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
@@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () =
   | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
-  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
+  Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)