diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-28 16:56:41 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-28 16:57:55 +0100 |
| commit | 110f7b41eca9c3e22fff0df67419b57d9c2ef612 (patch) | |
| tree | 3c19a09a5c08f6df478c99c1d34d5189e56b1310 | |
| parent | f1dd27ae0e6082b111770fa74cba6abda30f3b89 (diff) | |
Fix test suite after Matthieu's ed7af646f2e486b.
| -rw-r--r-- | test-suite/success/univnames.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v index 31d264f64..048b53d26 100644 --- a/test-suite/success/univnames.v +++ b/test-suite/success/univnames.v @@ -21,6 +21,6 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. -Universe g. +Monomorphic Universe g. Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file |