From b882fc5097c81071cfb0edf3a78cee10f3570c23 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Dec 2004 13:33:08 +0000
Subject: Ajout suffixe 8 pour test en nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6446 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.out  | 16 ----------------
 test-suite/output/Notations.out8 | 16 ++++++++++++++++
 test-suite/output/Notations.v    | 22 ----------------------
 test-suite/output/Notations.v8   | 22 ++++++++++++++++++++++
 4 files changed, 38 insertions(+), 38 deletions(-)
 delete mode 100644 test-suite/output/Notations.out
 create mode 100644 test-suite/output/Notations.out8
 delete mode 100644 test-suite/output/Notations.v
 create mode 100644 test-suite/output/Notations.v8

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
deleted file mode 100644
index 0e57e269d9..0000000000
--- a/test-suite/output/Notations.out
+++ /dev/null
@@ -1,16 +0,0 @@
-true ? 0; 1
-     : nat
-if true as x return (x ? nat; bool) then 0 else true
-     : true ? nat; bool
-Defining 'proj1' as keyword
-fun e : nat * nat => proj1 e
-     : nat * nat -> nat
-Defining 'decomp' as keyword
-decomp (true, true) as t, u in (t, u)
-     : (bool * bool)%type
-!(0 = 0)
-     : Prop
-forall n : nat, n = 0
-     : Prop
-!(0 = 0)
-     : Prop
diff --git a/test-suite/output/Notations.out8 b/test-suite/output/Notations.out8
new file mode 100644
index 0000000000..0e57e269d9
--- /dev/null
+++ b/test-suite/output/Notations.out8
@@ -0,0 +1,16 @@
+true ? 0; 1
+     : nat
+if true as x return (x ? nat; bool) then 0 else true
+     : true ? nat; bool
+Defining 'proj1' as keyword
+fun e : nat * nat => proj1 e
+     : nat * nat -> nat
+Defining 'decomp' as keyword
+decomp (true, true) as t, u in (t, u)
+     : (bool * bool)%type
+!(0 = 0)
+     : Prop
+forall n : nat, n = 0
+     : Prop
+!(0 = 0)
+     : Prop
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
deleted file mode 100644
index e5b469dba7..0000000000
--- a/test-suite/output/Notations.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(* Submitted by Roland Zumkeller *)
-
-Notation "a ? b ; c" := (if a then b else c) (at level 10).
-
-Check (true ? 0 ; 1).
-Check if true as x return (if x then nat else bool) then 0 else true.
-
-Notation "'proj1' t" := (let (a,_) := t in a) (at level 1).
-
-Check (fun e : nat * nat => proj1 e).
-
-Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1).
-
-Check (decomp (true,true) as t, u in (t,u)).
-
-(* Submitted by Roland Zumkeller *)
-
-Notation "! A" := (forall _:nat, A) (at level 60).
-
-Check ! (0=0).
-Check forall n, n=0.
-Check forall n:nat, 0=0.
diff --git a/test-suite/output/Notations.v8 b/test-suite/output/Notations.v8
new file mode 100644
index 0000000000..e5b469dba7
--- /dev/null
+++ b/test-suite/output/Notations.v8
@@ -0,0 +1,22 @@
+(* Submitted by Roland Zumkeller *)
+
+Notation "a ? b ; c" := (if a then b else c) (at level 10).
+
+Check (true ? 0 ; 1).
+Check if true as x return (if x then nat else bool) then 0 else true.
+
+Notation "'proj1' t" := (let (a,_) := t in a) (at level 1).
+
+Check (fun e : nat * nat => proj1 e).
+
+Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1).
+
+Check (decomp (true,true) as t, u in (t,u)).
+
+(* Submitted by Roland Zumkeller *)
+
+Notation "! A" := (forall _:nat, A) (at level 60).
+
+Check ! (0=0).
+Check forall n, n=0.
+Check forall n:nat, 0=0.
-- 
cgit v1.2.3