From 72b5c9d35dddf774c1d517889cb8f48a932d7095 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Mar 2015 22:29:38 +0100
Subject: Fixing computation of non-recursively uniform arguments in the
 presence of let-ins. This fixes #3491.

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v
new file mode 100644
index 0000000000..fd394ddbc3
--- /dev/null
+++ b/test-suite/bugs/closed/3491.v
@@ -0,0 +1,4 @@
+(* Was failing while building the _rect scheme, due to wrong computation of *)
+(* the number of non recursively uniform parameters in the presence of let-ins*)
+Inductive list (A : Type) (T := A) : Type :=
+    nil : list A | cons : T -> list T -> list A.
-- 
cgit v1.2.3


From c801b004bcb71f4f1db5d4cf260ef5a01fc8dde0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Mar 2015 22:52:10 +0100
Subject: Updating test-suite (see previous commit).

---
 test-suite/bugs/opened/3491.v | 2 --
 1 file changed, 2 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3491.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v
deleted file mode 100644
index 9837b0ecb2..0000000000
--- a/test-suite/bugs/opened/3491.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail Inductive list (A : Type) (T := A) : Type :=
-    nil : list A | cons : T -> list T -> list A.
-- 
cgit v1.2.3


From 598ac5ca1ac87fbd9152c7da1812a6ae7aa1e7bb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 29 Mar 2015 15:16:09 +0200
Subject: Adding test for bug #4165.

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4165.v b/test-suite/bugs/closed/4165.v
new file mode 100644
index 0000000000..8e0a62d35c
--- /dev/null
+++ b/test-suite/bugs/closed/4165.v
@@ -0,0 +1,7 @@
+Lemma foo : True.
+Proof.
+pose (fun x : nat => (let H:=true in x)) as s.
+match eval cbv delta [s] in s with
+| context C[true] =>
+  let C':=context C[false] in pose C' as s'
+end.
-- 
cgit v1.2.3