From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 test-suite/output/Notations.out | 24 +++++++++++++++++++
 test-suite/output/Notations.v   | 53 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 3ab3de45..be4cd4fa 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -14,6 +14,12 @@ forall n : nat, n = 0
      : Prop
 !(0 = 0)
      : Prop
+forall n : nat, #(n = n)
+     : Prop
+forall n n0 : nat, ##(n = n0)
+     : Prop
+forall n n0 : nat, ###(n = n0)
+     : Prop
 3 + 3
      : Z
 3 + 3
@@ -22,3 +28,21 @@ forall n : nat, n = 0
      : list nat
 (1; 2, 4)
      : nat * nat * nat
+Defining 'ifzero' as keyword
+ifzero 3
+     : bool
+Defining 'pred' as keyword
+pred 3
+     : nat
+fun n : nat => pred n
+     : nat -> nat
+fun n : nat => pred n
+     : nat -> nat
+Defining 'ifn' as keyword
+Defining 'is' as keyword
+fun x : nat => ifn x is succ n then n else 0
+     : nat -> nat
+1-
+     : bool
+-4
+     : Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 4382975e..3cc0a189 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -17,12 +17,33 @@ Check (decomp (true,true) as t, u in (t,u)).
 (**********************************************************************)
 (* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
 
+Section A.
+
 Notation "! A" := (forall _:nat, A) (at level 60).
 
 Check ! (0=0).
 Check forall n, n=0.
 Check forall n:nat, 0=0.
 
+End A.
+
+(**********************************************************************)
+(* Behaviour wrt to binding variables (cf bug report #1186)           *)
+
+Section B.
+
+Notation "# A" := (forall n:nat, n=n->A) (at level 60).
+Check forall n:nat, # (n=n).
+
+Notation "## A" := (forall n n0:nat, n=n0->A) (at level 60).
+Check forall n n0:nat, ## (n=n0).
+
+Notation "### A" :=
+ (forall n n0:nat, match n with O => True | S n => n=n0 end ->A) (at level 60).
+Check forall n n0:nat, ### (n=n0).
+
+End B.
+
 (**********************************************************************)
 (* Conflict between notation and notation below coercions             *)
 
@@ -66,3 +87,35 @@ Check [1;2;4].
 Reserved Notation "( x ; y , .. , z )" (at level 0).
 Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
 Check (1;2,4).
+
+(* Check basic notations involving "match" *)
+
+Section C.
+
+Notation "'ifzero' n" := (match n with 0 => true | S _ => false end)
+  (at level 0, n at level 0).
+Check (ifzero 3).
+
+Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end)
+  (at level 0, n at level 0).
+Check (pred 3).
+Check (fun n => match n with 0 => 0 | S n => n end).
+Check (fun n => match n with S p as x => p | y => 0 end).
+
+Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := 
+  (match x with O => u | S n => t end) (at level 0, u at level 0).
+Check fun x => ifn x is succ n then n else 0.
+
+End C.
+
+(* Check correction of bug #1179 *)
+
+Notation "1 -" := true (at level 0).
+Check 1-.
+
+(* This is another aspect of bug #1179 (raises anomaly in 8.1) *)
+
+Require Import ZArith.
+Open Scope Z_scope.
+Notation "- 4" := (-2 + -2).
+Check -4.
-- 
cgit v1.2.3