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.mli | |
| 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.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 0d0f3c0e5..fc9f25f96 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -69,3 +69,6 @@ val check_evar_instance : val remove_instance_local_defs : evar_map -> existential_key -> constr array -> constr list + +val get_type_of_refresh : + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types |