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 From 622c663094717530bc767dacce44b39041b9a732 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 Jul 2016 13:56:02 +0200 Subject: Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack). --- proofs/pfedit.ml | 2 +- tactics/extratactics.ml4 | 26 ++++++++++++++++++++++---- 2 files changed, 23 insertions(+), 5 deletions(-) (limited to 'proofs/pfedit.ml') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 20cae84a4..d3162c54f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -215,7 +215,7 @@ let refine_by_tactic env sigma ty tac = (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) -let implicit_tactic = ref None +let implicit_tactic = Summary.ref None ~name:"implicit-tactic" let declare_implicit_tactic tac = implicit_tactic := Some tac diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 15613c7ec..92d0ac983 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -525,11 +525,29 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF [ add_transitivity_lemma false t ] END +let cache_implicit_tactic (_,tac) = match tac with + | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) + | None -> Pfedit.clear_implicit_tactic () + +let subst_implicit_tactic (subst,tac) = + Option.map (Tacsubst.subst_tactic subst) tac + +let inImplicitTactic : glob_tactic_expr option -> obj = + declare_object {(default_object "IMPLICIT-TACTIC") with + open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); + cache_function = cache_implicit_tactic; + subst_function = subst_implicit_tactic; + classify_function = (fun o -> Dispose)} + +let declare_implicit_tactic tac = + Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) + +let clear_implicit_tactic () = + Lib.add_anonymous_leaf (inImplicitTactic None) + VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> - [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] -| [ "Clear" "Implicit" "Tactic" ] -> - [ Pfedit.clear_implicit_tactic () ] +| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ] +| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ] END -- cgit v1.2.3