From f5e0f609c8c2c77205fcfb296535a7d8856db584 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 15 Sep 2015 15:20:47 +0200
Subject: STM: Reset takes Ltac <ident> into account (Close #4316)

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4316.v b/test-suite/bugs/closed/4316.v
new file mode 100644
index 0000000000..68dec1334a
--- /dev/null
+++ b/test-suite/bugs/closed/4316.v
@@ -0,0 +1,3 @@
+Ltac tac := idtac.
+Reset tac.
+Ltac tac := idtac.
-- 
cgit v1.2.3


From dffd1a75c7ecf8870935f48c8aff2a9e750be4aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Sep 2015 16:39:24 +0200
Subject: Test for bug #4269.

---
 test-suite/output/PrintAssumptions.out |  2 ++
 test-suite/output/PrintAssumptions.v   | 16 ++++++++++++++++
 2 files changed, 18 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 23f33081b4..66458543aa 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -16,3 +16,5 @@ extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
 Closed under the global context
 Closed under the global context
+Axioms:
+M.foo : False
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index f23bc49808..c2003816ca 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -94,3 +94,19 @@ Proof (false_positive.add_comm 5).
 
 Print Assumptions comm_plus5.
 (* Should answer : Closed under the global context *)
+
+(** Print Assumption and Include *)
+
+Module INCLUDE.
+
+Module M.
+Axiom foo : False.
+End M.
+
+Module N.
+Include M.
+End N.
+
+Print Assumptions N.foo.
+
+End INCLUDE.
-- 
cgit v1.2.3


From 16db94e6c142217a81cc78be8788137617c24de7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 16 Sep 2015 21:44:47 +0200
Subject: In pat/constr introduction patterns, fixing in a better way clearing
 problems of temporary hypotheses than 76f27140e6e34 did.

---
 test-suite/success/intros.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index ae1694c58c..35ba94fb67 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -61,3 +61,11 @@ Goal forall n, n = S n -> 0=0.
 intros n H/n_Sn.
 destruct H.
 Qed.
+
+(* Another check about generated names and cleared hypotheses with
+   pat/c patterns *)
+Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
+intros H (H1,?)/H.
+change (1=1) in H0.
+exact H1.
+Qed.
-- 
cgit v1.2.3