diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /tactics/eauto.ml4 | |
| parent | 2ed87ba29db49e043062e125f3783a553d550fc4 (diff) | |
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 310b70fd9..c450bf622 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -29,6 +29,7 @@ open Pattern open Clenv open Auto open Rawterm +open Hiddentac let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 or occur_existential t2 then @@ -54,13 +55,6 @@ let registered_e_assumption gl = tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) (pf_ids_of_hyps gl)) gl -(* This automatically define h_eApply (among other things) *) -TACTIC EXTEND eapply - [ "eapply" constr_with_bindings(c) ] -> [ Tactics.eapply_with_bindings c ] -END - -let simplest_eapply c = h_eapply (c,NoBindings) - let e_constructor_tac boundopt i lbind gl = let cl = pf_concl gl in let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in @@ -130,8 +124,8 @@ END let one_step l gl = [Tactics.intro] - @ (List.map simplest_eapply (List.map mkVar (pf_ids_of_hyps gl))) - @ (List.map simplest_eapply l) + @ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl))) + @ (List.map h_simplest_eapply l) @ (List.map assumption (pf_ids_of_hyps gl)) let rec prolog l n gl = @@ -162,7 +156,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 - simplest_eapply c gls + h_simplest_eapply c gls let rec e_trivial_fail_db db_list local_db goal = let tacl = |