diff options
| author | Matthieu Sozeau | 2014-04-07 13:07:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:59 +0200 |
| commit | 484e2c349e68b0284f278f691334d82001ee0f0e (patch) | |
| tree | 929910f466ed8cadbf6bb8a7b470e49f7f187190 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions