diff options
author | 2017-07-17 15:07:39 +0200 | |
---|---|---|
committer | 2017-07-17 15:07:39 +0200 | |
commit | eba5d64fee0bf6235265f1f6cc884b4cbefe2704 (patch) | |
tree | 9c8950e67e27c3d781bc1d69a0d4066eadd845b5 /engine/universes.mli | |
parent | c707b52613d650cac665aaf252a449ab25ce9351 (diff) | |
parent | 839e87fffdf2634b841aeba6de6d36a2d7a27dbd (diff) |
Merge PR #783: Remove some useless code in Term_typing
Diffstat (limited to 'engine/universes.mli')
0 files changed, 0 insertions, 0 deletions