10 files changed, 61 insertions, 48 deletions
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.out b/test-suite/output/Notations.out
index b60b1ee863..94b86fc222 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -125,13 +125,15 @@ s
      : nat
 fun _ : nat => 9
      : nat -> nat
-fun (x : nat) (p : x = x) => match p with
-                             | ONE => ONE
-                             end = p
+fun (x : nat) (p : x = x) =>
+match p in (_ = n) return (n = n) with
+| ONE => ONE
+end = p
      : forall x : nat, x = x -> Prop
-fun (x : nat) (p : x = x) => match p with
-                             | 1 => 1
-                             end = p
+fun (x : nat) (p : x = x) =>
+match p in (_ = n) return (n = n) with
+| 1 => 1
+end = p
      : forall x : nat, x = x -> Prop
 bar  0
      : nat
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/Quote.v b/test-suite/output/Quote.v
deleted file mode 100644
index 2c373d5052..0000000000
--- a/test-suite/output/Quote.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Require Import Quote.
-
-Parameter A B : Prop.
-
-Inductive formula : Type :=
-  | f_and : formula -> formula -> formula
-  | f_or : formula -> formula -> formula
-  | f_not : formula -> formula
-  | f_true : formula
-  | f_atom : index -> formula
-  | f_const : Prop -> formula.
-
-Fixpoint interp_f (vm:
-                    varmap Prop) (f:formula) {struct f} : Prop :=
-  match f with
-  | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
-  | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
-  | f_not f1 => ~ interp_f vm f1
-  | f_true => True
-  | f_atom i => varmap_find True i vm
-  | f_const c => c
-  end.
-
-Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B).
-intro H.
-match goal with
-  | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H)
-end.
-match goal with
-  |- ?g => quote interp_f [ A ] in g using (fun x => idtac x)
-end.
-quote interp_f.
-Show.
-simpl; quote interp_f [ A ].
-Show.
-Admitted.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 6f41b2fcf9..926114a1e1 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -48,6 +48,12 @@ Type@{Top.17} -> Type@{v} -> Type@{u}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
+Type@{i} -> Type@{j}
+     : Type@{max(i+1,j+1)}
+(* {j i} |=  *)
+     = Type@{i} -> Type@{j}
+     : Type@{max(i+1,j+1)}
+(* {j i} |=  *)
 Monomorphic mono = Type@{mono.u}
      : Type@{mono.u+1}
 (* {mono.u} |=  *)
@@ -149,24 +155,24 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i}
-(* i Top.44 Top.45 |=  *)
+axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i}
-(* i Top.44 Top.45 |=  *)
+axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.47} -> Type@{axbar'.i}
+axfoo' : Type@{Top.51} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.47} -> Type@{axbar'.i}
+axbar' : Type@{Top.51} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index c6efc240a6..f806a9f4f7 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -30,6 +30,11 @@ Unset Strict Universe Declaration.
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+
+Check Type@{i} -> Type@{j}.
+
+Eval cbv in Type@{i} -> Type@{j}.
+
 Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
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.