12 files changed, 100 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b8aac8b6f8..f5ec80bcfc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -106,7 +106,8 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-te
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log \
-  prerequisite/bind_univs.v.log
+  prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \
+  prerequisite/module_bug7192.v.log
 
 #######################################################################
 # Phony targets
diff --git a/test-suite/bugs/closed/8270.v b/test-suite/bugs/closed/8270.v
new file mode 100644
index 0000000000..f36f757f10
--- /dev/null
+++ b/test-suite/bugs/closed/8270.v
@@ -0,0 +1,15 @@
+(* Don't do zeta in cbn when not asked for *)
+
+Goal let x := 0 in
+     let y := x in
+     y = 0.
+  (* We use "cofix" as an example because there are obviously no
+     cofixpoints in sight.  This problem arises with any set of
+     reduction flags (not including zeta where the lets are of course reduced away) *)
+  cbn cofix.
+  intro x.
+  unfold x at 1. (* Should succeed *)
+  Undo 2.
+  cbn zeta.
+  Fail unfold x at 1.
+Abort.
diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v
new file mode 100644
index 0000000000..0350be9c06
--- /dev/null
+++ b/test-suite/bugs/closed/8288.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Set Polymorphic Inductive Cumulativity.
+
+Inductive foo := C : (forall A : Type -> Type, A Type) -> foo.
+(* anomaly invalid subtyping relation *)
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index bd9240476f..b67ac4f0df 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -10,6 +10,8 @@ Arguments Nat.sub !n !m.
 About Nat.sub.
 Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
   fun x => (f (fst x), g (snd x)).
+Declare Scope foo_scope.
+Declare Scope bar_scope.
 Delimit Scope foo_scope with F.
 Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
 About pf.
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index fe6c05c39e..adab324cf0 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -76,6 +76,7 @@ Open Scope nat_scope.
 Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
 Coercion Zpos: nat >-> znat.
 
+Declare Scope znat_scope.
 Delimit Scope znat_scope with znat.
 Open Scope znat_scope.
 
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 34f44cd246..3f4d5ef58c 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -20,3 +20,5 @@ Axioms:
 M.foo : False
 Closed under the global context
 Closed under the global context
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index ea1ab63786..3d4dfe603d 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -137,3 +137,13 @@ Module F (X : T).
 End F.
 
 End SUBMODULES.
+
+(* Testing a variant of #7192 across files *)
+(* This was missing in the original fix to #7192 *)
+Require Import module_bug7192.
+Print Assumptions M7192.D.f.
+
+(* Testing reporting assumptions from modules in files *)
+(* A regression introduced in the original fix to #7192 was missing implementations *)
+Require Import module_bug8416.
+Print Assumptions M8416.f.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index eb9f571022..efdc94fb1e 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -38,3 +38,14 @@ Ltac foo :=
   let w := () in
   let z := 1 in
   pose v
+2 subgoals
+  
+  n : nat
+  ============================
+  (fix a (n0 : nat) : nat := match n0 with
+                             | 0 => 0
+                             | S n1 => a n1
+                             end) n = n
+
+subgoal 2 is:
+ forall a : nat, a = 0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 901b1e3aa6..40e743c3f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -71,3 +71,13 @@ Ltac foo :=
   let z := 1 in
   pose v.
 Print Ltac foo.
+
+(* Ltac renaming was not applied to "fix" and "cofix" *)
+
+Goal forall a, a = 0.
+match goal with
+|- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n)
+end.
+intro.
+Show.
+Abort.
diff --git a/test-suite/prerequisite/module_bug7192.v b/test-suite/prerequisite/module_bug7192.v
new file mode 100644
index 0000000000..82cfe560af
--- /dev/null
+++ b/test-suite/prerequisite/module_bug7192.v
@@ -0,0 +1,9 @@
+(* Variant of #7192 to be tested in a file requiring this file *)
+(* #7192 is about Print Assumptions not entering implementation of submodules *)
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module M7192: C.
+  Module D <: B. Definition f := a. End D.
+End M7192.
diff --git a/test-suite/prerequisite/module_bug8416.v b/test-suite/prerequisite/module_bug8416.v
new file mode 100644
index 0000000000..70f43d132a
--- /dev/null
+++ b/test-suite/prerequisite/module_bug8416.v
@@ -0,0 +1,2 @@
+Module Type A. Axiom f : True. End A.
+Module M8416 : A. Definition f := I. End M8416.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0f22a1f0a0..4404ff3f16 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -348,3 +348,32 @@ symmetry in H.
 match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
 exact (eq_refl H0).
 Abort.
+
+(* Check that internal names used in "match" compilation to push "term
+   to match" on the environment are not interpreted as ltac variables *)
+
+Module ToMatchNames.
+Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac.
+Goal True.
+g 1.
+Abort.
+End ToMatchNames.
+
+(* An example where internal names used to build the return predicate
+   (here "n" because "a" is bound to "nil" and "n" is the first letter
+   of "nil") by small inversion should be taken distinct from Ltac names. *)
+
+Module LtacNames.
+Inductive t (A : Type) : nat -> Type :=
+    nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n).
+
+Ltac f a n :=
+  let x := constr:(match a with nil _ => true | cons _ _ _ _ => I end) in
+  assert (x=x/\n=n).
+
+Goal forall (y:t nat 0), True.
+intros.
+f y true.
+Abort.
+
+End LtacNames.