diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-01 23:32:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-02 00:07:10 +0200 |
| commit | 68846802a7be637ec805a5e374655a426b5723a5 (patch) | |
| tree | eb9a170bb94c96f3a50203d8d941823a23743064 /pretyping/evarsolve.ml | |
| parent | cf36105854c9a42960ee4139c6afdaa75ec8f31a (diff) | |
Work around issues with FO unification trying to unify terms of
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.
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 *) (************************) |