diff options
| author | Matthieu Sozeau | 2014-06-21 16:14:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-21 16:14:59 +0200 |
| commit | 14ae5f4534ee5e632d82990e7db76305b9ca9b75 (patch) | |
| tree | 7ba63a0f2de145d04dddf01e17e25beeebbc72f6 /lib/control.ml | |
| parent | 9b3a234e4cf002292ca4a67e1b72daac463b4c46 (diff) | |
- Add an option to refresh only algebraic universes, for e_type_of. The goal
there is not the same as in Evd.define.
- Fixed bugs #3330 and #3331.
Diffstat (limited to 'lib/control.ml')
0 files changed, 0 insertions, 0 deletions