diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 13:07:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:59 +0200 |
| commit | 484e2c349e68b0284f278f691334d82001ee0f0e (patch) | |
| tree | 929910f466ed8cadbf6bb8a7b470e49f7f187190 /test-suite/success/RecTutorial.v | |
| parent | 4bc936b22f9ed1e90286f39c8d51c9f05c37b300 (diff) | |
- Fix RecTutorial, and mutual induction schemes getting the wrong names.
Now the universe inconsistency appears at [exact t] instead of the Defined :)
Diffstat (limited to 'test-suite/success/RecTutorial.v')
| -rw-r--r-- | test-suite/success/RecTutorial.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 15af08442..11fbf24d4 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -520,8 +520,7 @@ Inductive typ : Type := Definition typ_inject: typ. split. -exact typ. -Fail Defined. +Fail exact typ. (* Error: Universe Inconsistency. *) |