Merge branch 'v8.5'

8 files changed, 74 insertions, 17 deletions

diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v
new file mode 100644
index 0000000000..eb0d206c5c
--- /dev/null
+++ b/test-suite/bugs/closed/3779.v
@@ -0,0 +1,11 @@
+Set Universe Polymorphism.
+Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
+Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
+Section foo.
+  Universes sm lg.
+  Context (O : UnitSubuniverse@{sm lg}).
+  Context {A : Type@{sm}}.
+  Context (H' : forall (C : Type@{lg}) `{In@{sm lg} O C} (f : A -> C), In@{sm lg} O C).
+  Fail Check (H' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+  Fail Context (H'' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+End foo.
diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v
new file mode 100644
index 0000000000..bc120fb1ff
--- /dev/null
+++ b/test-suite/bugs/closed/4221.v
@@ -0,0 +1,9 @@
+(* Some test checking that interpreting binder names using ltac
+   context does not accidentally break the bindings *)
+
+Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
+  intros H0 x.
+  lazymatch goal with
+    | [ x : forall k : nat, _ |- _ ]
+      => specialize (fun H0 => x 1 H0)
+  end.
diff --git a/test-suite/bugs/closed/4254.v b/test-suite/bugs/closed/4254.v
new file mode 100644
index 0000000000..ef219973df
--- /dev/null
+++ b/test-suite/bugs/closed/4254.v
@@ -0,0 +1,13 @@
+Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+
+Module WithPoly.
+Polymorphic Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+End WithPoly.
diff --git a/test-suite/interactive/4289.v b/test-suite/interactive/4289.v
new file mode 100644
index 0000000000..610a509c9b
--- /dev/null
+++ b/test-suite/interactive/4289.v
@@ -0,0 +1,14 @@
+(* Checking backtracking with modules which used to fail due to an
+   hash-consing bug *)
+
+Module Type A.
+  Axiom B : nat.
+End A.
+Module C (a : A).
+  Include a.
+  Definition c : nat := B.
+End C.
+Back 4.
+Module C (a : A).
+  Include a.
+  Definition c : nat := B.
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index 0d75d52a31..0d75d52a31 100755..100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 0d75d52a31..0d75d52a31 100755..100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a4ed76c5a0..074004fa12 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -333,13 +333,10 @@ exact (refl_equal 3).
 exact (refl_equal 4).
 Qed.
 
-(* From 12612, descent in conjunctions is more powerful *)
+(* From 12612, Dec 2009, descent in conjunctions is more powerful *)
 (* The following, which was failing badly in bug 1980, is now
    properly rejected, as descend in conjunctions builds an
-   ill-formed elimination from Prop to Type.
-
-   Added Aug 2014: why it fails is now that trivial unification ?x = goal is
-   rejected by the descent in conjunctions to avoid surprising results. *)
+   ill-formed elimination from Prop to the domain of ex which is in Type. *)
 
 Goal True.
 Fail eapply ex_intro.
@@ -351,28 +348,32 @@ Fail eapply (ex_intro _).
 exact I.
 Qed.
 
-(* Note: the following succeed directly (i.e. w/o "exact I") since
-   Aug 2014 since the descent in conjunction does not use a "cut"
-   anymore: the iota-redex is contracted and we get rid of the
-   uninstantiated evars
-
-   Is it good or not? Maybe it does not matter so much.
+(* No failure here, because the domain of ex is in Prop *)
 
 Goal True.
-eapply (ex_intro (fun _ => True) I).    
-exact I. (* Not needed since Aug 2014 *)
+eapply (ex_intro (fun _ => 0=0) I).
+reflexivity.
 Qed.
 
 Goal True.
-eapply (ex_intro (fun _ => True) I _).    
-exact I. (* Not needed since Aug 2014 *)
+eapply (ex_intro (fun _ => 0=0) I _).
+Unshelve. (* In 8.4:  Grab Existential Variables. *)
+reflexivity.
 Qed.
 
 Goal True.
 eapply (fun (A:Prop) (x:A) => conj I x).
-exact I. (* Not needed since Aug 2014 *)
+Unshelve. (* In 8.4: the goal ?A was there *)
+exact I.
 Qed.
-*)
+
+(* Testing compatibility mode with v8.4 *)
+
+Goal True.
+Fail eapply existT.
+Set Universal Lemma Under Conjunction.
+eapply existT.
+Abort.
 
 (* The following was not accepted from r12612 to r12657 *)
 
@@ -463,6 +464,7 @@ Abort.
 Goal forall H:0=0, H = H.
 intros.
 Fail apply eq_sym in H.
+Abort.
 
 (* Check that unresolved evars not originally present in goal prevent
    apply in to work*)
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index badce063e8..f9df021dc2 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -298,3 +298,11 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
+
+(* Check instantiation of binders using ltac names *)
+
+Goal True.
+let x := ipattern:y in assert (forall x y, x = y + 0).
+intro.
+destruct y. (* Check that the name is y here *)
+Abort.