Merge branch 'v8.6'

10 files changed, 52 insertions, 16 deletions

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
new file mode 100644
index 0000000000..75dd38fde8
--- /dev/null
+++ b/test-suite/.csdp.cache
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 *)
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.
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.
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.
diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache
deleted file mode 100644
index 8e5708cf02..0000000000
--- a/test-suite/csdp.cache
+++ /dev/null
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
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
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).