diff options
| author | Vincent Laporte | 2018-10-03 14:02:51 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-04 08:27:31 +0000 |
| commit | d19372209eca556bb07116b518d8740ff6385035 (patch) | |
| tree | 83fff45b8e00c35f4242c90e2a7ec19ece38579d /test-suite/success/unidecls.v | |
| parent | 1e4ac27962aaab5132c9294156ac2a0da9652a43 (diff) | |
Test-suite: avoid explicit references to “Top”
Diffstat (limited to 'test-suite/success/unidecls.v')
| -rw-r--r-- | test-suite/success/unidecls.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v index 014f1834a2..7c298c98b6 100644 --- a/test-suite/success/unidecls.v +++ b/test-suite/success/unidecls.v @@ -1,3 +1,4 @@ +(* coq-prog-args: ("-top" "unidecls") *) Set Printing Universes. Module decls. @@ -39,7 +40,7 @@ Check Type@{Foo.bar}. Check Type@{Foo.foo}. (** The same *) Check Type@{foo}. -Check Type@{Top.foo}. +Check Type@{unidecls.foo}. Universe secfoo. Section Foo'. |