From 36f3ae391ee188edb9d858d8832d7fd611db0482 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 21 Feb 2017 12:56:28 +0100
Subject: Univs: fix bug #5365, generation of u+k <= v constraints

Use an explicit label ~algebraic for make_flexible_variable as well.
---
 test-suite/bugs/closed/5365.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/5365.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v
new file mode 100644
index 0000000000..be360d24d2
--- /dev/null
+++ b/test-suite/bugs/closed/5365.v
@@ -0,0 +1,13 @@
+
+Inductive TupleT : nat -> Type :=
+| nilT : TupleT 0
+| consT {n} A : (A -> TupleT n) -> TupleT (S n).
+
+Inductive Tuple : forall n, TupleT n -> Type :=
+  nil : Tuple _ nilT
+| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).
+
+Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
+  tmNil : TupleMap _ nilT nilT
+| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n)
+  : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G).
-- 
cgit v1.2.3


From 09cbae6c995c3e94ac8f0e53e6857da8e491a2fe Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 8 Jun 2017 14:54:39 +0200
Subject: Adding a test case as requested in bug 5205.

---
 test-suite/bugs/closed/5205.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/5205.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v
new file mode 100644
index 0000000000..406f37a4b1
--- /dev/null
+++ b/test-suite/bugs/closed/5205.v
@@ -0,0 +1,6 @@
+Definition foo (n : nat) (m : nat) : nat := m.
+
+Arguments foo {_} _, _ _.
+
+Check foo 1 1.
+Check foo (n:=1) 1.
-- 
cgit v1.2.3