aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Nametab.out
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-27 12:10:04 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-09-27 12:10:04 +0000
commit2069ddbed501da4f24203d3fb92187e012ab582d (patch)
treee29d9b1ec828157064f8b25e2e9167913f9f3298 /test-suite/output/Nametab.out
parent6a9f037bad58c73aff5a972b36a2d5549ab37e71 (diff)
Encore quelques rangements dans Nametab + petits trucs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3039 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Nametab.out')
-rw-r--r--test-suite/output/Nametab.out28
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
new file mode 100644
index 000000000..505821d7e
--- /dev/null
+++ b/test-suite/output/Nametab.out
@@ -0,0 +1,28 @@
+id is not a defined object
+K.id is not a defined object
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+K is not a defined object
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q
+id is not a defined object
+Constant Top.Q.N.K.id
+N.K.id is not a defined object
+Constant Top.Q.N.K.id
+Constant Top.Q.N.K.id
+Module Top.Q.N.K
+N.K is not a defined object
+Module Top.Q.N.K
+Module Top.Q.N.K
+N is not a defined object
+Module Top.Q.N
+Module Top.Q.N
+Module Top.Q
+Module Top.Q