diff options
| author | Gaëtan Gilbert | 2018-11-09 16:42:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-09 16:43:42 +0100 |
| commit | a1895a5b58aa0f06235ca1619ac0acd1fab78780 (patch) | |
| tree | 0202fdc502a55a0d4711f1f3abc711176a2ed3e3 | |
| parent | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (diff) | |
Fix -top for univbinders output test.
It was good enough for the makefile but not for emacs.
| -rw-r--r-- | test-suite/output/UnivBinders.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 19d241d35d..ad901da72f 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,4 +1,5 @@ -(* coq-prog-args: ("-top" "UnivBinders") *) +(* -*- coq-prog-args: ("-top" "UnivBinders"); -*- *) + Set Universe Polymorphism. Set Printing Universes. (* Unset Strict Universe Declaration. *) |