From 2b4517cf85432d68e53ac46815309fd8068a40ad Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 28 Aug 2016 19:43:00 +0200
Subject: Fix bug #4764: Syntactic notation externalization breaks.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v
new file mode 100644
index 0000000000..e545cc1b71
--- /dev/null
+++ b/test-suite/bugs/closed/4764.v
@@ -0,0 +1,5 @@
+Notation prop_fun x y := (fun (x : Prop) => y).
+Definition foo := fun (p : Prop) => p.
+Definition bar := fun (_ : Prop) => O.
+Print foo.
+Print bar.
-- 
cgit v1.2.3


From 44ada644ef50563aa52cfcd7717d44bde29e5a20 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 17:37:27 +0200
Subject: Fix bug #3920: eapply masks an hypothesis name.

The problem came from the fact that the legacy beta-reduction occurring
after a rewrite was wrongly applied to the side-conditions of the
rewriting step. We restrict it to the correct goal in this patch.
---
 test-suite/bugs/closed/3920.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/3920.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v
new file mode 100644
index 0000000000..a4adb23cc2
--- /dev/null
+++ b/test-suite/bugs/closed/3920.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+Axiom P : nat -> Prop.
+Axiom P_or : forall x y, P (x + y) <-> P x \/ P y.
+Lemma foo (H : P 3) : False.
+eapply or_introl in H.
+erewrite <- P_or in H.
+(* Error: No such hypothesis: H *)
-- 
cgit v1.2.3


From 721637c98514a77d05d080f53f226cab3a8da1e7 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Tue, 30 Aug 2016 17:12:27 +0200
Subject: plugin micromega : nra also handles non-linear rational arithmetic
 over Q (Fixed #4985)

Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.
---
 test-suite/micromega/qexample.v | 17 +++++++++--------
 test-suite/micromega/rexample.v | 12 ++++++------
 2 files changed, 15 insertions(+), 14 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 47e6005b94..d001e8f7fc 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -6,32 +6,29 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Psatz.
+Require Import Lqa.
 Require Import QArith.
 
 Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
 Proof.
   intros.
-  psatzl Q.
+  lra.
 Qed.
 
-
-
-
 (* Other (simple) examples *)
 Open Scope Q_scope.
 
 Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2).
 Proof.
   intros.
-  psatzl Q.
+  lra.
 Qed.
 
 
 Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m.
 Proof.
-  intros ; psatzl Q.
+  intros ; lra.
 Qed.
 Open Scope Z_scope.
 Open Scope Q_scope.
@@ -60,7 +57,11 @@ Lemma vcgen_25 : forall
   (( 1# 1) == (-2 # 1) * i + it).
 Proof.
   intros.
-  psatzl Q.
+  lra.
+Qed.
+
+Goal forall x : Q, x * x >= 0.
+  intro; nra. 
 Qed.
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 2eed7e951d..89c08c7704 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -6,7 +6,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Psatz.
+Require Import Lra.
 Require Import Reals.
 
 Open Scope R_scope.
@@ -15,7 +15,7 @@ Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 (* Other (simple) examples *)
@@ -23,13 +23,13 @@ Qed.
 Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
-  intros ; psatzl R.
+  intros ; lra.
 Qed.
 
 
@@ -57,7 +57,7 @@ Lemma vcgen_25 : forall
   (( 1 ) = (-2  ) * i + it).
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
@@ -72,5 +72,5 @@ Proof.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
-intros; split_Rabs; psatzl R.
+intros; split_Rabs; lra.
 Qed.
\ No newline at end of file
-- 
cgit v1.2.3


From 4582ed1c8f0620941a3c296941b1dc808c95d7fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 18:47:45 +0200
Subject: Fix bug #4893: not_evar: unexpected failure in 8.5pl1.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v
new file mode 100644
index 0000000000..9a35bcf954
--- /dev/null
+++ b/test-suite/bugs/closed/4893.v
@@ -0,0 +1,4 @@
+Goal True.
+evar (P: Prop).
+assert (H : P); [|subst P]; [exact I|].
+let T := type of H in not_evar T.
-- 
cgit v1.2.3


From 68ee3958437b98291d69709b9c2a730abf7f7f96 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 19:01:17 +0200
Subject: Fixing output test-suite after warning for inner Requires.

---
 test-suite/output/PatternsInBinders.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index b5c91e347b..fff86d6fae 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -1,3 +1,5 @@
+Require Coq.Unicode.Utf8.
+
 (** The purpose of this file is to test printing of the destructive
     patterns used in binders ([fun] and [forall]). *)
 
@@ -37,7 +39,7 @@ End WithParameters.
 (** Some test involving unicode notations. *)
 Module WithUnicode.
 
-  Require Import Coq.Unicode.Utf8.
+  Import Coq.Unicode.Utf8.
 
   Check λ '((x,y) : A*B),  (y,x).
   Check ∀ '(x,y), swap (x,y) = (y,x).
-- 
cgit v1.2.3


From 12268bef28dea57fdbe29dc87d26ef453ad5cfed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 31 Aug 2016 11:32:28 +0200
Subject: Fix bug #5043: [Admitted] lemmas pick up section variables.

We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
---
 test-suite/bugs/closed/5043.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/5043.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v
new file mode 100644
index 0000000000..4e6a0f878f
--- /dev/null
+++ b/test-suite/bugs/closed/5043.v
@@ -0,0 +1,8 @@
+Unset Keep Admitted Variables.
+
+Section a.
+  Context (x : Type).
+  Definition foo : Type.
+  Admitted.
+End a.
+Check foo : Type.
-- 
cgit v1.2.3


From 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Wed, 31 Aug 2016 19:12:15 +0200
Subject: Fix Bug #5005 : micromega tactics is now robust to failure of
 'abstract'.

If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
---
 test-suite/micromega/zomicron.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 0ec1dbfbcd..1f148becc9 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -33,4 +33,13 @@ Lemma compact_proof : forall z,
 Proof.
  intros.
  lia.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma dummy_ex : exists (x:Z),  x = x.
+Proof.
+  eexists.
+  lia.
+  Unshelve.
+  exact Z0.
+Qed.
+  
\ No newline at end of file
-- 
cgit v1.2.3


From af2df1ada04da94a41a400c637788db461a532d9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 1 Sep 2016 17:40:16 +0200
Subject: Fix test-suite after Frédéric's 6231f07b2.

---
 test-suite/.csdp.cache | Bin 0 -> 79491 bytes
 test-suite/csdp.cache  | Bin 79491 -> 0 bytes
 2 files changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 test-suite/.csdp.cache
 delete mode 100644 test-suite/csdp.cache

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
new file mode 100644
index 0000000000..75dd38fde8
Binary files /dev/null and b/test-suite/.csdp.cache differ
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
deleted file mode 100644
index 8e5708cf02..0000000000
Binary files a/test-suite/csdp.cache and /dev/null differ
-- 
cgit v1.2.3