Merge branch 'v8.5' into trunk

4 files changed, 29 insertions, 0 deletions

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.
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.
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.