From c487e02b0b8bffbe3135d7024f25d03a2f5f1af4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 29 Jul 2015 16:37:29 +0200
Subject: Adding test for bug #3779.

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

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 5a6e0088adb4e817133d4d7f5a547fbc23fe7951 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 30 Jul 2015 14:00:12 +0200
Subject: Test file for bug #4289 (buggy hash-consing of kernel name pairs
 breaking backtracking in the presence of functors).

In "interactive" rather than "bugs" because of the use of Back.
---
 test-suite/interactive/4289.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/interactive/4289.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 505eb0f0dae9b8a6ac810070d60916b67942b305 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 31 Jul 2015 09:34:48 +0200
Subject: Remove some outdated files and fix permissions.

---
 test-suite/interactive/ParalITP_smallproofs.v    | 0
 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 mode change 100755 => 100644 test-suite/interactive/ParalITP_smallproofs.v
 mode change 100755 => 100644 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v

(limited to 'test-suite')

diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
old mode 100755
new mode 100644
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
old mode 100755
new mode 100644
-- 
cgit v1.2.3


From 2418cf8d5ff6f479a5b43a87c861141bf9067507 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jul 2015 21:31:37 +0200
Subject: Granting Jason's request for an ad hoc compatibility option on
 considering trivial unifications "?x = t" in tactics working under
 conjunctions (see #3545).

Also updating and fixing wrong comments in test apply.v.
---
 test-suite/success/apply.v | 36 +++++++++++++++++++-----------------
 1 file changed, 19 insertions(+), 17 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a4ed76c5a0..24d5cf8a99 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 Trivial Tactic Unification 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*)
-- 
cgit v1.2.3


From 817308ab59daa40bef09838cfc3d810863de0e46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 16:53:39 +0200
Subject: Fixing #4221 (interpreting bound variables using ltac env was
 possibly capturing bound names unexpectingly).

We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").

We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in

let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).

which was producing

forall z : nat, match z with 0 => z | S y => y end = 0

because the names in default branches are treated specifically.

It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).

However, we rename binders in fix which were not interpreted.

There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).

fix ltac name
---
 test-suite/bugs/closed/4221.v | 9 +++++++++
 test-suite/success/ltac.v     | 8 ++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/4221.v

(limited to 'test-suite')

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/success/ltac.v b/test-suite/success/ltac.v
index badce063e8..952f35bc35 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.
-- 
cgit v1.2.3


From 164637cc3a4e8895ed4ec420e300bd692d3e7812 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 18:47:08 +0200
Subject: Fixing test apply.v (had wrong option name).

---
 test-suite/success/apply.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 24d5cf8a99..074004fa12 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -371,7 +371,7 @@ Qed.
 
 Goal True.
 Fail eapply existT.
-Set Trivial Tactic Unification Under Conjunction.
+Set Universal Lemma Under Conjunction.
 eapply existT.
 Abort.
 
-- 
cgit v1.2.3


From 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 19:31:00 +0200
Subject: Reverting 16 last commits, committed mistakenly using the wrong push
 command. Sorry so much.

Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
---
 test-suite/success/apply.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 074004fa12..24d5cf8a99 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -371,7 +371,7 @@ Qed.
 
 Goal True.
 Fail eapply existT.
-Set Universal Lemma Under Conjunction.
+Set Trivial Tactic Unification Under Conjunction.
 eapply existT.
 Abort.
 
-- 
cgit v1.2.3


From 47b4573a77ef88f8528c8247108eba8b04d81525 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 18:47:08 +0200
Subject: Fixing test apply.v (had wrong option name).

---
 test-suite/success/apply.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 24d5cf8a99..074004fa12 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -371,7 +371,7 @@ Qed.
 
 Goal True.
 Fail eapply existT.
-Set Trivial Tactic Unification Under Conjunction.
+Set Universal Lemma Under Conjunction.
 eapply existT.
 Abort.
 
-- 
cgit v1.2.3


From 97fba91264669d495643f6a3de6a09790ae2a1da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 21:08:12 +0200
Subject: Continuing 817308ab (use ltac env for terms in ltac context) + fix of
 syntax in test file ltac.v.

---
 test-suite/success/ltac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 952f35bc35..f9df021dc2 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -304,5 +304,5 @@ Abort.
 Goal True.
 let x := ipattern:y in assert (forall x y, x = y + 0).
 intro.
-destruct y. (* Check that the name is y here *).
+destruct y. (* Check that the name is y here *)
 Abort.
-- 
cgit v1.2.3


From dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 3 Aug 2015 10:31:48 +0200
Subject: Test file for #4254: Mutual inductives with parameters on Type raises
 anomaly.

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

(limited to 'test-suite')

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.
-- 
cgit v1.2.3