12 files changed, 235 insertions, 8 deletions
diff --git a/test-suite/README.md b/test-suite/README.md
index ef2e574ece..e81da0830f 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -62,20 +62,26 @@ BUILDING SUMMARY FILE
 NO FAILURES
 ```
 
-See [`test-suite/Makefile`](/test-suite/Makefile) for more information.
+See [`test-suite/Makefile`](Makefile) for more information.
 
 ## Adding a test
 
-Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number.
+Regression tests for closed bugs should be added to
+[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number.
 Files in this directory are tested for successful compilation.
 When you fix a bug, you should usually add a regression test here as well.
 
-The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile.
+The error "(bug seems to be opened, please check)" when running
+`make test-suite` means that a test in [`bugs/closed`](bugs/closed) failed to
+compile.
 
-There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output.
+There are also output tests in [`output`](output) which consist of a `.v` file
+and a `.out` file with the expected output.
 
-There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
-unit-test framework, as described at http://ounit.forge.ocamlcore.org/.  Use `make unit-tests' in the unit-tests directory to run them.
+There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests
+are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as
+described at <http://ounit.forge.ocamlcore.org/>.  Use `make unit-tests` in the
+[`unit-tests`](unit-tests) directory to run them.
 
 ## Fixing output tests
 
@@ -88,5 +94,5 @@ automatically.
 Don't forget to check the updated `.out` files into git!
 
 Note that `output/MExtraction.out` is special: it is copied from
-`micromega/micromega.ml` in the plugin source directory. Automatic
-approval will incorrectly update the copy.
+[`micromega/micromega.ml`](../plugins/micromega/micromega.ml) in the plugin
+source directory. Automatic approval will incorrectly update the copy.
diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
index 2ee438934e..54c75e344c 100644
--- a/test-suite/bugs/closed/2800.v
+++ b/test-suite/bugs/closed/2800.v
@@ -4,3 +4,16 @@ intuition
   match goal with
   | |- _ => idtac " foo"
   end.
+
+  lazymatch goal with _ => idtac end.
+  match goal with _ => idtac end.
+  unshelve lazymatch goal with _ => idtac end.
+  unshelve match goal with _ => idtac end.
+  unshelve (let x := I in idtac).
+Abort.
+
+Require Import ssreflect.
+
+Goal True.
+match goal with _ => idtac end => //.
+Qed.
diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v
new file mode 100644
index 0000000000..aa63e2ab0e
--- /dev/null
+++ b/test-suite/bugs/closed/5500.v
@@ -0,0 +1,35 @@
+(* Too weak check on the correctness of return clause was leading to an anomaly *)
+
+Inductive Vector A: nat -> Type :=
+  nil: Vector A O
+| cons: forall n, A -> Vector A n -> Vector A (S n).
+
+(* This could be made working with a better inference of inner return
+   predicates from the return predicate at the higher level of the
+   nested matching. Currently, we only check that it does not raise an
+   anomaly, but eventually, the "Fail" could be removed. *)
+
+Fail Definition hd_fst A x n (v: A * Vector A (S n)) :=
+  match v as v0 return match v0 with
+                       (l, r) =>
+                       match r in Vector _ n return match n with 0 => Type | S _ => Type end with
+                         nil _ => A
+                       | cons _ _ _ _ => A
+                       end
+                       end with
+    (_, nil _) => x
+  | (_, cons _ n hd tl) => hd
+  end.
+
+(* This is another example of failure but involving beta-reduction and
+   not iota-reduction. Thus, for this one, I don't see how it could be
+   solved by small inversion, whatever smart is small inversion. *)
+
+Inductive A : (Type->Type) -> Type := J : A (fun x => x).
+
+Fail Check fun x : nat * A (fun x => x) =>
+  match x return match x with
+                 (y,z) => match z in A f return f Type with J => bool end
+                 end with
+  (y,J) => true
+  end.
diff --git a/test-suite/bugs/closed/5547.v b/test-suite/bugs/closed/5547.v
new file mode 100644
index 0000000000..79633f4893
--- /dev/null
+++ b/test-suite/bugs/closed/5547.v
@@ -0,0 +1,16 @@
+(* Checking typability of intermediate return predicates in nested pattern-matching *)
+
+Inductive A : (Type->Type) -> Type := J : A (fun x => x).
+Definition ret (x : nat * A (fun x => x))
+  := match x return Type with
+     | (y,z) => match z in A f return f Type with
+                | J => bool
+                end
+     end.
+Definition foo : forall x, ret x.
+Proof.
+Fail refine (fun x
+          => match x return ret x with
+             | (y,J) => true
+             end
+         ).
diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v
new file mode 100644
index 0000000000..cd8c4ad7df
--- /dev/null
+++ b/test-suite/bugs/closed/7615.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type S.
+Parameter Inline T@{i} : Type@{i+1}.
+End S.
+
+Module F (X : S).
+Definition X@{j i} : Type@{j} := X.T@{i}.
+End F.
+
+Module M.
+Definition T@{i} := Type@{i}.
+End M.
+
+Module N := F(M).
+
+Require Import Hurkens.
+
+Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.
diff --git a/test-suite/bugs/closed/7700.v b/test-suite/bugs/closed/7700.v
new file mode 100644
index 0000000000..56f5481baa
--- /dev/null
+++ b/test-suite/bugs/closed/7700.v
@@ -0,0 +1,9 @@
+(* Abbreviations to section variables were not located *)
+Section foo.
+  Let x := Set.
+  Notation y := x.
+  Check y.
+  Variable x' : Set.
+  Notation y' := x'.
+  Check y'.
+End foo.
diff --git a/test-suite/bugs/closed/7779.v b/test-suite/bugs/closed/7779.v
new file mode 100644
index 0000000000..78936b5958
--- /dev/null
+++ b/test-suite/bugs/closed/7779.v
@@ -0,0 +1,15 @@
+(* Checking that the "in" clause takes the "eqn" clause into account *)
+
+Definition test (x: nat): {y: nat | False }. Admitted.
+
+Parameter x: nat.
+Parameter z: nat.
+
+Goal
+  proj1_sig (test x) = z ->
+  False.
+Proof.
+  intro H.
+  destruct (test x) eqn:Heqs in H.
+  change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
+Abort.
diff --git a/test-suite/bugs/closed/7780.v b/test-suite/bugs/closed/7780.v
new file mode 100644
index 0000000000..2318f4d6ec
--- /dev/null
+++ b/test-suite/bugs/closed/7780.v
@@ -0,0 +1,16 @@
+(* A lift was missing in expanding aliases under binders for unification *)
+
+(* Below, the lift was missing while expanding the reference to
+   [mkcons] in [?N] which was under binder [arg] *)
+
+Goal forall T (t : T) (P P0 : T -> Set), option (option (list (P0 t)) -> option (list (P t))).
+  intros ????.
+  refine (Some
+            (fun rls
+             => let mkcons := ?[M] in
+                let default arg := ?[N] in
+                match rls as rls (* 2 *) return option (list (P ?[O])) with
+                | Some _ => None
+                | None => None
+                end)).
+Abort.
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 66458543aa..34f44cd246 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -18,3 +18,5 @@ Closed under the global context
 Closed under the global context
 Axioms:
 M.foo : False
+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 c2003816ca..ea1ab63786 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -110,3 +110,30 @@ End N.
 Print Assumptions N.foo.
 
 End INCLUDE.
+
+(* Print Assumptions did not enter implementation of submodules (#7192) *)
+
+Module SUBMODULES.
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module E: C.
+  Module D <: B. Definition f := a. End D.
+End E.
+Print Assumptions E.D.f.
+
+(* Idem in the scope of a functor *)
+
+Module Type T. End T.
+Module F (X : T).
+  Definition a := True.
+  Module Type B. Axiom f : Prop. End B.
+  Module Type C. Declare Module D : B. End C.
+  Module E: C.
+    Module D <: B. Definition f := a. End D.
+  End E.
+  Print Assumptions E.D.f.
+End F.
+
+End SUBMODULES.
diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out
new file mode 100644
index 0000000000..a57b3bbad5
--- /dev/null
+++ b/test-suite/output/Unicode.out
@@ -0,0 +1,41 @@
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+        f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) 
+        (z : very_very_long_type_name2), f y x ∧ f y z
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1) 
+        (z : very_very_long_type_name2),
+        f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z
+1 subgoal
+  
+  very_very_long_type_name1 : Type
+  very_very_long_type_name2 : Type
+  f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+  ============================
+  True
+  → True
+    → ∃ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+        f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
diff --git a/test-suite/output/Unicode.v b/test-suite/output/Unicode.v
new file mode 100644
index 0000000000..42b07e5a08
--- /dev/null
+++ b/test-suite/output/Unicode.v
@@ -0,0 +1,28 @@
+Require Import Coq.Unicode.Utf8.
+
+Section test.
+Context (very_very_long_type_name1 : Type) (very_very_long_type_name2 : Type).
+Context (f : very_very_long_type_name1 -> very_very_long_type_name2 -> Prop).
+
+Lemma test : True -> True ->
+  forall (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+    f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+  forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+         (z : very_very_long_type_name2),
+    f y x /\ f y z.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+  forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+         (z : very_very_long_type_name2),
+    f y x /\ f y z /\ f y x /\ f y z /\ f y x /\ f y z.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+  exists (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+    f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
+Proof. Show. Abort.
+End test.