diff options
| author | Matthieu Sozeau | 2014-06-25 11:41:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-25 11:41:21 +0200 |
| commit | b8b6970da464ebd222f05992f77da641bf98591d (patch) | |
| tree | f7c4991633ced80fe24258d67cde2f053625e0e0 | |
| parent | 0dac8434c9f4190becfd8f169e588fc0270f5397 (diff) | |
Use full transparent state when checking well-typedness of a second order matching
infered predicate, instead of the arguments ts which might be empty (e.g. in unification).
Fixes failure in success/unification.v
| -rw-r--r-- | pretyping/evarconv.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2761dcbe33..e9d152de2d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -882,7 +882,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = force_instantiation evd !evsref | [] -> let evd = - try Evarsolve.check_evar_instance evd evk rhs (evar_conv_x ts) + try Evarsolve.check_evar_instance evd evk rhs + (evar_conv_x full_transparent_state) with IllTypedInstance _ -> raise (TypingFailed evd) in Evd.define evk rhs evd |