From 68ee3958437b98291d69709b9c2a730abf7f7f96 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Aug 2016 19:01:17 +0200
Subject: Fixing output test-suite after warning for inner Requires.

---
 test-suite/output/PatternsInBinders.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index b5c91e347b..fff86d6fae 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -1,3 +1,5 @@
+Require Coq.Unicode.Utf8.
+
 (** The purpose of this file is to test printing of the destructive
     patterns used in binders ([fun] and [forall]). *)
 
@@ -37,7 +39,7 @@ End WithParameters.
 (** Some test involving unicode notations. *)
 Module WithUnicode.
 
-  Require Import Coq.Unicode.Utf8.
+  Import Coq.Unicode.Utf8.
 
   Check λ '((x,y) : A*B),  (y,x).
   Check ∀ '(x,y), swap (x,y) = (y,x).
-- 
cgit v1.2.3