aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.v
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-19 20:34:48 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-22 15:10:46 +0200
commit96bb190caa138c91b4d5e5f96d6f179811a177c8 (patch)
treea42eab7717b7abf753665dee814f0b31b6ab8a07 /test-suite/output/Notations2.v
parent1c506bb3d9128590f23a4872586a22d930672a69 (diff)
Fixing output test Notations2.
Diffstat (limited to 'test-suite/output/Notations2.v')
-rw-r--r--test-suite/output/Notations2.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index c9efe1ead..4e0d135d7 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -71,7 +71,6 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
Module A.
Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
Check fun f x => f x + S x.
-End A.
Open Scope list_scope.
Notation list1 := (1::nil)%list.
@@ -79,6 +78,7 @@ Notation plus2 n := (S (S n)).
(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
Print plus2.
Check fun n => match n with list1 => 0 | _ => 2 end.
+End A.
(* This one is not fully satisfactory because binders in the same type
are re-factorized and parentheses are needed even for atomic binder