diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-08 16:57:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-08 17:04:48 +0200 |
| commit | 32dc4dc94c5677bc686a16a4a047f1750d0d8582 (patch) | |
| tree | dc1794d73f3ad4bad978e1c56c43f67bff6b347f /pretyping/miscops.mli | |
| parent | 8b093fa1828eee800da2bc73de33ea8804175924 (diff) | |
Fix documentation of universes.
Diffstat (limited to 'pretyping/miscops.mli')
0 files changed, 0 insertions, 0 deletions