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/evarutil.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/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 4 |
1 files changed, 2 insertions, 2 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 |