diff options
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
3 files changed, 8 insertions, 3 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index be1d52a6c9..ad31f5d3b2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -63,7 +63,7 @@ let registered_e_assumption gl = (* This automatically define h_eApply (among other things) *) TACTIC EXTEND eapply - [ "eapply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ] + [ "eapply" constr_with_bindings(c) ] -> [ Tactics.eapply_with_bindings c ] END let vernac_e_resolve_constr c = h_eapply (c,NoBindings) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f9e623469e..5a5e8989ef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -509,7 +509,7 @@ let cut_in_parallel l = (* Resolution with missing arguments *) -let apply_with_bindings (c,lbind) gl = +let apply_with_bindings_gen with_evars (c,lbind) gl = (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -519,7 +519,8 @@ let apply_with_bindings (c,lbind) gl = let n = nb_prod thm_ty - nb_prod (pf_concl gl) 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 - Clenvtac.res_pf clause gl + 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 @@ -532,6 +533,9 @@ let apply_with_bindings (c,lbind) gl = let clause = make_clenv_binding_apply gl None (c,thm_ty0) lbind in Clenvtac.res_pf clause gl +let apply_with_bindings = apply_with_bindings_gen false +let eapply_with_bindings = apply_with_bindings_gen true + let apply c = apply_with_bindings (c,NoBindings) let apply_list = function diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ac51f736c1..c44b683f36 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -167,6 +167,7 @@ val apply : constr -> tactic val apply_without_reduce : constr -> tactic val apply_list : constr list -> tactic val apply_with_bindings : constr with_bindings -> tactic +val eapply_with_bindings : constr with_bindings -> tactic val cut_and_apply : constr -> tactic |