From dae240f31d6de1d5b3737d6d0779e009f3d67fa2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 Jul 2016 12:48:26 +0200 Subject: Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars). But there are still bugs with Declare Implicit Tactic, which should probably rather be reimplemented with ltac:(tac). Indeed, it does support evars in the type of the term, and solve_by_implicit_tactic should transfer universe constraints to the main goal. E.g., the following still fails, at Qed time. Definition Foo {T}{a : T} : T := a. Declare Implicit Tactic eassumption. Goal forall A (x : A), A. intros. apply Foo. Qed. --- proofs/pfedit.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a515c9e75..20cae84a4 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 -- cgit v1.2.3