diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b2cf21b818..ac1692f451 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -694,7 +694,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst = (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) if with_evars then - let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in + let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in + let idcl' = List.filter f idcl in match idcl' with | [c,_,id] -> begin |