aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-21 22:40:06 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-21 22:40:06 +0000
commitb73047dadb0b915ec9108285e6cd28bd73cde2fd (patch)
tree8e9dcf742528226417a96d7ee0adf522ab08376a
parentecc45c8526274ca8659cb264df0c232e420078d6 (diff)
Anciennement déplacé dans 'output'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7687 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--test-suite/modules/Nametab.v48
1 files changed, 0 insertions, 48 deletions
diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
deleted file mode 100644
index 61966c7c8..000000000
--- a/test-suite/modules/Nametab.v
+++ /dev/null
@@ -1,48 +0,0 @@
-Module Q.
- Module N.
- Module K.
- Definition id:=Set.
- End K.
- End N.
-End Q.
-
-(* Bad *) Locate id.
-(* Bad *) Locate K.id.
-(* Bad *) Locate N.K.id.
-(* OK *) Locate Q.N.K.id.
-(* OK *) Locate Top.Q.N.K.id.
-
-(* Bad *) Locate K.
-(* Bad *) Locate N.K.
-(* OK *) Locate Q.N.K.
-(* OK *) Locate Top.Q.N.K.
-
-(* Bad *) Locate N.
-(* OK *) Locate Q.N.
-(* OK *) Locate Top.Q.N.
-
-(* OK *) Locate Q.
-(* OK *) Locate Top.Q.
-
-
-
-Import Q.N.
-
-
-(* Bad *) Locate id.
-(* OK *) Locate K.id.
-(* Bad *) Locate N.K.id.
-(* OK *) Locate Q.N.K.id.
-(* OK *) Locate Top.Q.N.K.id.
-
-(* OK *) Locate K.
-(* Bad *) Locate N.K.
-(* OK *) Locate Q.N.K.
-(* OK *) Locate Top.Q.N.K.
-
-(* Bad *) Locate N.
-(* OK *) Locate Q.N.
-(* OK *) Locate Top.Q.N.
-
-(* OK *) Locate Q.
-(* OK *) Locate Top.Q.