diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a515c9e750..20cae84a49 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -230,8 +230,10 @@ let solve_by_implicit_tactic env sigma evk = (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in (try + let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, _) = - build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in + build_by_tactic env (Evd.evar_universe_context sigma) c tac in ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit |