From 1ef6104cf043ec839059cddfe530a81418a3d474 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Jul 2016 13:45:32 +0200
Subject: Add test file for #4880.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v
new file mode 100644
index 0000000000..5569798d54
--- /dev/null
+++ b/test-suite/bugs/closed/4880.v
@@ -0,0 +1,11 @@
+Require Import Coq.Reals.Reals Coq.nsatz.Nsatz.
+Local Open Scope R.
+
+Goal forall x y : R,
+  x*x =  y *  y ->
+  x*x = -y * -y ->
+  x*(x*x) = 0 -> (* The associativity does not actually matter, *)
+  (x*x)*x = 0.   (* just otherwise [assumption] would solve the goal. *)
+Proof.
+  nsatz.
+Qed.
-- 
cgit v1.2.3


From 88f4ca3d1798fc28f230f749665bcf48597accc3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 7 Jul 2016 13:48:20 +0200
Subject: Test file for #4858.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v
new file mode 100644
index 0000000000..c04895a1bb
--- /dev/null
+++ b/test-suite/bugs/closed/4858.v
@@ -0,0 +1,7 @@
+Require Import Nsatz.
+Goal True.
+nsatz_compute
+ (PEc 0%Z :: PEc (-1)%Z
+    :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1
+       :: PEsub (PEX Z 1) (PEX Z 1) :: nil).
+Abort.
-- 
cgit v1.2.3


From b0e81d65b85c1846a961196d70cd86ede2993c5b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 8 Jul 2016 10:40:03 +0200
Subject: Update csdp.cache.

---
 test-suite/csdp.cache | Bin 79491 -> 79491 bytes
 1 file changed, 0 insertions(+), 0 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 75dd38fde8..8e5708cf02 100644
Binary files a/test-suite/csdp.cache and b/test-suite/csdp.cache differ
-- 
cgit v1.2.3


From e1661dc9a43b34526437e9bc3029e6320e09f899 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 8 Jul 2016 13:03:16 +0200
Subject: Fix test file for #4858.

---
 test-suite/bugs/closed/4858.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v
index c04895a1bb..a2fa93832a 100644
--- a/test-suite/bugs/closed/4858.v
+++ b/test-suite/bugs/closed/4858.v
@@ -1,6 +1,6 @@
 Require Import Nsatz.
 Goal True.
-nsatz_compute
+try nsatz_compute
  (PEc 0%Z :: PEc (-1)%Z
     :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1
        :: PEsub (PEX Z 1) (PEX Z 1) :: nil).
-- 
cgit v1.2.3


From 65ba1b36df33a74998240a02fecc1fb80c3eeeee Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Jul 2016 15:27:28 +0200
Subject: Fixing printing of evar name in an error message of instantiate.

---
 test-suite/output/Errors.out | 2 ++
 test-suite/output/Errors.v   | 9 +++++++++
 2 files changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 6354ad469e..8048deb0c0 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -5,3 +5,5 @@ Unable to unify "nat" with "True".
 The command has indeed failed with message:
 In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
+The command has indeed failed with message:
+Error: Instance is not well-typed in the environment of ?x
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 352c87385f..424d24801c 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -16,3 +16,12 @@ Goal True.
 Fail simpl; apply 0.
 Fail simpl; f 0.
 Abort.
+
+(* Test instantiate error messages *)
+
+Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
+intros T1 P1 H1.
+eexists ?[x].
+destruct H1 as [x1 H1].
+Fail instantiate (x:=projT1 x1).
+Abort.
-- 
cgit v1.2.3