aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/PatternsInBinders.v
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-08-30 19:01:17 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-08-30 19:03:05 +0200
commit68ee3958437b98291d69709b9c2a730abf7f7f96 (patch)
tree1396aa35c7917ebcfe2870ceeb64b10b6ac963ce /test-suite/output/PatternsInBinders.v
parent4582ed1c8f0620941a3c296941b1dc808c95d7fe (diff)
Fixing output test-suite after warning for inner Requires.
Diffstat (limited to 'test-suite/output/PatternsInBinders.v')
-rw-r--r--test-suite/output/PatternsInBinders.v4
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index b5c91e347..fff86d6fa 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).