diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 6818d84fe..83462d4c4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1040,9 +1040,10 @@ let check_evar_instance evd evk1 body conv_algo = let evi = Evd.find evd evk1 in let evenv = evar_env evi in (* FIXME: The body might be ill-typed when this is called from w_merge *) + (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = - try Retyping.get_type_of evenv evd body - with e when Errors.noncritical e -> error "Ill-typed evar instance" + try Retyping.get_type_of ~lax:true evenv evd body + with Retyping.RetypeError _ -> error "Ill-typed evar instance" in match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd |