From 5009be2f117a5ef27733b7d6895503af91e9aa34 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 14 Oct 2015 15:57:42 +0200
Subject: When typechecking a lemma statement, try to resolve typeclasses
 before failing for unresolved evars (regression).

---
 stm/lemmas.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 5cbe152b55..c49ddfd8ec 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),
-- 
cgit v1.2.3