diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-06-21 16:14:59 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-21 16:14:59 +0200 |
commit | 14ae5f4534ee5e632d82990e7db76305b9ca9b75 (patch) | |
tree | 7ba63a0f2de145d04dddf01e17e25beeebbc72f6 /pretyping/typing.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 'pretyping/typing.ml')
-rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7702355b8..1c41a5bb3 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes false env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type else !evdref, j.uj_type let solve_evars env evdref c = |