Universe binders survive sections, modules and compilation.

4 files changed, 75 insertions, 1 deletions

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}.