diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-01 17:20:55 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 23:31:08 +0200 |
| commit | 5de89439d459edd402328a1e437be4d8cd2e4f46 (patch) | |
| tree | f473c0f26b211c1ca31259e3fd85acf12ff42769 | |
| 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).
| -rw-r--r-- | pretyping/evarutil.ml | 4 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 5 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
3 files changed, 4 insertions, 7 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b0718ed7e..d14aa23a7 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -126,7 +126,7 @@ let nf_evar_map_undefined evm = (* Auxiliary functions for the conversion algorithms modulo evars *) -let has_undefined_evars or_sorts evd t = +let has_undefined_evars evd t = let rec has_ev t = match kind_of_term t with | Evar (ev,args) -> @@ -140,7 +140,7 @@ let has_undefined_evars or_sorts evd t = with (Not_found | NotInstantiatedEvar) -> true let is_ground_term evd t = - not (has_undefined_evars true evd t) + not (has_undefined_evars evd t) let is_ground_env evd env = let is_ground_decl = function diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 3876b0d3e..fc27d4776 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -79,9 +79,8 @@ val head_evar : constr -> existential_key (** may raise NoHeadEvar *) (* Expand head evar if any *) val whd_head_evar : evar_map -> constr -> constr -(* [has_undefined_evars or_sorts evd c] checks if [c] has undefined evars - and optionally if it contains undefined sorts. *) -val has_undefined_evars : bool -> evar_map -> constr -> bool +(* [has_undefined_evars evd c] checks if [c] has undefined evars. *) +val has_undefined_evars : evar_map -> constr -> bool val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool (** [check_evars env initial_sigma extended_sigma c] fails if some diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b358d6302..df669f5be 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 |