diff options
| author | herbelin | 2007-04-15 20:18:08 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-15 20:18:08 +0000 |
| commit | d6168dc0ce49d146635183d70c9ccb40e77784de (patch) | |
| tree | 3304f08f2e682672827f96c78846142175e1f4f4 | |
| parent | e6134e05461345934b6b22bbf564a241f5a2d13c (diff) | |
Essai de partage de code entre apply et eapply
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9770 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |