diff options
| -rw-r--r-- | proofs/pfedit.ml | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 35 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4882.v | 50 |
3 files changed, 84 insertions, 7 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a515c9e750..d3162c54f2 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 @@ -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 diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 15613c7ecc..06fea367af 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -345,11 +345,18 @@ END (**********************************************************************) (* Refine *) +let constr_flags = { + Pretyping.use_typeclasses = true; + Pretyping.use_unif_heuristics = true; + Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic; + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } + let refine_tac simple {Glob_term.closure=closure;term=term} = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let flags = Pretyping.all_no_fail_flags in + let flags = constr_flags in let tycon = Pretyping.OfType concl in let lvar = { Pretyping.empty_lvar with Pretyping.ltac_constrs = closure.Glob_term.typed; @@ -525,11 +532,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 diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v new file mode 100644 index 0000000000..8c26af708b --- /dev/null +++ b/test-suite/bugs/closed/4882.v @@ -0,0 +1,50 @@ + +Definition Foo {T}{a : T} : T := a. + +Module A. + + Declare Implicit Tactic eauto. + + Goal forall A (x : A), A. + intros. + apply Foo. (* Check defined evars are normalized *) + (* Qed. *) + Abort. + +End A. + +Module B. + + Definition Foo {T}{a : T} : T := a. + + Declare Implicit Tactic eassumption. + + Goal forall A (x : A), A. + intros. + apply Foo. + (* Qed. *) + Abort. + +End B. + +Module C. + + Declare Implicit Tactic first [exact True|assumption]. + + Goal forall (x : True), True. + intros. + apply (@Foo _ _). + Qed. + +End C. + +Module D. + + Declare Implicit Tactic assumption. + + Goal forall A (x : A), A. + intros. + exact _. + Qed. + +End D. |