diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-14 15:57:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-14 17:06:49 +0200 |
| commit | 5009be2f117a5ef27733b7d6895503af91e9aa34 (patch) | |
| tree | 230e09bd12bc4bdc4ddb4d0f5403d1306e176c2f | |
| parent | 5b67ba8e1bbd92d4ef7e2adab13bd05e7b55bfd7 (diff) | |
When typechecking a lemma statement, try to resolve typeclasses before
failing for unresolved evars (regression).
| -rw-r--r-- | stm/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5cbe152b5..c49ddfd8e 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -439,7 +439,7 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - check_evars_are_solved env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); let ids = List.map pi1 ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), |