From 391ce2bdd44418ffa07e199ba2e447428c45c3bd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Nov 2004 09:24:26 +0000
Subject: Test lieurs dans Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6309 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.out | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test-suite/output/Notations.out

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
new file mode 100644
index 0000000000..0e57e269d9
--- /dev/null
+++ b/test-suite/output/Notations.out
@@ -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
-- 
cgit v1.2.3