The semantics of Variable x y : T is to have the exact same type T for x and y,

while Context gives different type to each variable, this test-suite file shows this.

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_034.v b/test-suite/bugs/closed/HoTT_coq_034.v
new file mode 100644
index 000000000..ae665931a
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_034.v
@@ -0,0 +1,23 @@
+Module Short.
+  Set Universe Polymorphism.
+  Inductive relevant (A : Type) (B : Type) : Prop := .
+  Section foo.
+    Variables A B : Type.
+    Definition foo := prod (relevant A B) A.
+  End foo.
+
+  Section bar.
+    Variable A : Type.
+    Variable B : Type.
+    Definition bar := prod (relevant A B) A.
+  End bar.
+
+  Set Printing Universes.
+  Check bar nat Set : Set. (* success *)
+  Fail Check foo nat Set : Set. (* Toplevel input, characters 6-17:
+Error:
+The term "foo (* Top.303 Top.304 *) nat Set" has type
+"Type (* Top.304 *)" while it is expected to have type
+"Set" (Universe inconsistency: Cannot enforce Top.304 = Set because Set
+< Top.304)). *)
+End Short.