diff options
| author | Matthieu Sozeau | 2014-08-01 17:20:55 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-03 23:31:08 +0200 |
| commit | 5de89439d459edd402328a1e437be4d8cd2e4f46 (patch) | |
| tree | f473c0f26b211c1ca31259e3fd85acf12ff42769 /pretyping/unification.ml | |
| parent | 6dde48d3a75f3b8ffc960c4ac3f668ff93e93297 (diff) | |
- Fix has_undefined_evars not using its or_sorts argument anymore.
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b358d6302a..df669f5bef 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -36,8 +36,6 @@ let occur_meta_or_undefined_evar evd c = | Evar_defined c -> occrec c; Array.iter occrec args | Evar_empty -> raise Occur) - | Const (_, i) (* | Ind (_, i) | Construct (_, i) *) - when not (Univ.Instance.is_empty i) -> raise Occur | _ -> iter_constr occrec c in try occrec c; false with Occur | Not_found -> true |