diff options
| -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 b0718ed7ec..d14aa23a7e 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 3876b0d3e0..fc27d4776e 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 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 |