diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 15:07:39 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-17 15:07:39 +0200 |
| commit | eba5d64fee0bf6235265f1f6cc884b4cbefe2704 (patch) | |
| tree | 9c8950e67e27c3d781bc1d69a0d4066eadd845b5 /engine/universes.ml | |
| parent | c707b52613d650cac665aaf252a449ab25ce9351 (diff) | |
| parent | 839e87fffdf2634b841aeba6de6d36a2d7a27dbd (diff) | |
Merge PR #783: Remove some useless code in Term_typing
Diffstat (limited to 'engine/universes.ml')
0 files changed, 0 insertions, 0 deletions