diff options
-rw-r--r-- | tactics/eauto.ml4 | 17 | ||||
-rw-r--r-- | tactics/eauto.mli | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 27 |
3 files changed, 20 insertions, 28 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ad31f5d3b..310b70fd9 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -44,13 +44,6 @@ TACTIC EXTEND eassumption | [ "eassumption" ] -> [ e_assumption ] END -let e_resolve_with_bindings_tac (c,lbind) gl = - let t = pf_hnf_constr gl (pf_type_of gl c) in - let clause = make_clenv_binding_apply gl None (c,t) lbind in - Clenvtac.e_res_pf clause gl - -let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls - TACTIC EXTEND eexact | [ "eexact" constr(c) ] -> [ e_give_exact c ] END @@ -66,7 +59,7 @@ TACTIC EXTEND eapply [ "eapply" constr_with_bindings(c) ] -> [ Tactics.eapply_with_bindings c ] END -let vernac_e_resolve_constr c = h_eapply (c,NoBindings) +let simplest_eapply c = h_eapply (c,NoBindings) let e_constructor_tac boundopt i lbind gl = let cl = pf_concl gl in @@ -82,7 +75,7 @@ let e_constructor_tac boundopt i lbind gl = | None -> () end; let cons = mkConstruct (ith_constructor_of_inductive mind i) in - let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in + let apply_tac = eapply_with_bindings (cons,lbind) in (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast ; intros; apply_tac]) gl @@ -137,8 +130,8 @@ END let one_step l gl = [Tactics.intro] - @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl))) - @ (List.map e_resolve_constr l) + @ (List.map simplest_eapply (List.map mkVar (pf_ids_of_hyps gl))) + @ (List.map simplest_eapply l) @ (List.map assumption (pf_ids_of_hyps gl)) let rec prolog l n gl = @@ -169,7 +162,7 @@ open Auto let unify_e_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false clenv' gls in - vernac_e_resolve_constr c gls + simplest_eapply c gls let rec e_trivial_fail_db db_list local_db goal = let tacl = diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 4621088e2..d17afd293 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -22,10 +22,6 @@ val e_assumption : tactic val registered_e_assumption : tactic -val e_resolve_constr : constr -> tactic - -val vernac_e_resolve_constr : constr -> tactic - val e_give_exact_constr : constr -> tactic val gen_eauto : bool -> bool * int -> constr list -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5a5e8989e..c496ffe64 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -42,6 +42,7 @@ open Tacexpr open Decl_kinds open Evarutil open Indrec +open Pretype_errors exception Bound @@ -514,24 +515,26 @@ let apply_with_bindings_gen with_evars (c,lbind) gl = goal. If this fails, then the head constant will be unfolded step by step. *) let thm_ty0 = nf_betaiota (pf_type_of gl c) in + let concl_nprod = nb_prod (pf_concl gl) in let rec try_apply thm_ty = try - let n = nb_prod thm_ty - nb_prod (pf_concl gl) in + let n = nb_prod thm_ty - concl_nprod in if n<0 then error "Apply: theorem has not enough premisses."; let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in if with_evars then Clenvtac.e_res_pf clause gl else Clenvtac.res_pf clause gl - with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn -> - let red_thm = - try red_product (pf_env gl) (project gl) thm_ty - with (Redelimination | UserError _) -> raise exn in - try_apply red_thm in - try try_apply thm_ty0 - with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) -> - (* Last chance: if the head is a variable, apply may try - second order unification *) - let clause = make_clenv_binding_apply gl None (c,thm_ty0) lbind in - Clenvtac.res_pf clause gl + with PretypeError _|RefinerError _|UserError _|Failure _ -> + try + (* Try to head-reduce the conclusion of the theorem *) + let red_thm = try_red_product (pf_env gl) (project gl) thm_ty in + try_apply red_thm + with Redelimination -> + (* Last chance: if the head is a variable, apply may try + second order unification *) + let clause = make_clenv_binding_apply gl None (c,thm_ty) lbind in + if with_evars then Clenvtac.e_res_pf clause gl + else Clenvtac.res_pf clause gl in + try_apply thm_ty0 let apply_with_bindings = apply_with_bindings_gen false let eapply_with_bindings = apply_with_bindings_gen true |