diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a41e0169a..94ec82029 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -101,6 +101,10 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = in if !modified then !evdref, t' else !evdref, t +let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = + let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in + refresh_universes (Some false) env sigma ty + (************************) (* Unification results *) (************************) |