4 files changed, 98 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/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/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.