diff options
| author | Hugo Herbelin | 2015-07-16 21:34:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-16 21:43:53 +0200 |
| commit | 0b3a335219e161dc04f6734e9ee4f7c08cde6cd5 (patch) | |
| tree | 325ab45b64832fa7e55d85cf7446517d40fd04df | |
| parent | 916a8dc2c6b1dd8400d5c44b5d9c7fc793cc0e97 (diff) | |
Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
| -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 |