diff options
| author | Matthieu Sozeau | 2015-10-14 18:17:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-14 18:17:42 +0200 |
| commit | 26af31cb46c7baf92325dd22bf6ee33aaa2172d2 (patch) | |
| tree | 3adc9a34251ff69c74f1aa72e072df694e1f2306 | |
| parent | b8c681338cad546c397a1803c55183cc6526adfb (diff) | |
Occur-check in evar_define was not strong enough.
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 754ad8f588..bbc4f1db29 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1484,7 +1484,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = if occur_meta body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) - if occur_evar evk body then raise (OccurCheckIn (evd',body)); + if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in (* Cannot strictly type instantiations since the unification algorithm |