From 0e36e624975c743ac8164cfe00f3ab02f0624eb3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Dec 2005 21:32:06 +0000
Subject: Abandon tests syntaxe v7; remplacement des .v par des fichiers en
 syntaxe v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7701 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Nametab.out       | 36 ++++++++++++++++++++++++++++++++++++
 test-suite/output/Notations.out     | 16 ++++++++++++++++
 test-suite/output/TranspModtype.out | 10 ++++++++++
 3 files changed, 62 insertions(+)
 create mode 100644 test-suite/output/Nametab.out
 create mode 100644 test-suite/output/Notations.out
 create mode 100644 test-suite/output/TranspModtype.out

diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
new file mode 100644
index 0000000000..d0f15f0ed8
--- /dev/null
+++ b/test-suite/output/Nametab.out
@@ -0,0 +1,36 @@
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is Q.N.K.id)
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is Q.N.K.id)
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is Q.N.K.id)
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is Q.N.K.id)
+No module is referred to by basename K
+No module is referred to by name N.K
+Module Top.Q.N.K
+Module Top.Q.N.K
+No module is referred to by basename N
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is K.id)
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is K.id)
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is K.id)
+Constant Top.Q.N.K.id
+  (shorter name to refer to it in current context is K.id)
+Module Top.Q.N.K
+No module is referred to by name N.K
+Module Top.Q.N.K
+Module Top.Q.N.K
+No module is referred to by basename N
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
new file mode 100644
index 0000000000..3a2548dddc
--- /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
+!(0 = 0)
+     : Prop
+forall n : nat, n = 0
+     : Prop
+!(0 = 0)
+     : Prop
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
new file mode 100644
index 0000000000..41e8648bc0
--- /dev/null
+++ b/test-suite/output/TranspModtype.out
@@ -0,0 +1,10 @@
+TrM.A = M.A
+     : Set
+
+OpM.A = M.A
+     : Set
+
+TrM.B = M.B
+     : Set
+
+*** [ OpM.B : Set ]
-- 
cgit v1.2.3