5 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v
new file mode 100644
index 000000000..a2fa93832
--- /dev/null
+++ b/test-suite/bugs/closed/4858.v
@@ -0,0 +1,7 @@
+Require Import Nsatz.
+Goal True.
+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).
+Abort.
diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v
new file mode 100644
index 000000000..5569798d5
--- /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.
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
index 75dd38fde..8e5708cf0 100644
--- a/test-suite/csdp.cache
+++ b/test-suite/csdp.cache
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 6354ad469..62e9ef4b2 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -5,3 +5,6 @@ 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:
+Ltac call to "instantiate" failed.
+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 352c87385..424d24801 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.