diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 14:41:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 14:41:07 +0000 |
| commit | 97fb9f22eadab06fe320ccedf6abfb6be89702f4 (patch) | |
| tree | 39236d4d52b822faf79a4d665e79ac689dc3f978 /tactics/hiddentac.ml | |
| parent | b9f32144ada6df45194ea011b1c6468e10747c8f (diff) | |
Ajout "simple apply" et "simple eapply" pour apply sans unfold
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10738 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 60f1ccf0c..18263127b 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -39,9 +39,9 @@ let h_exact_no_check c = abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c) let h_vm_cast_no_check c = abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) -let h_apply ev cb = - abstract_tactic (TacApply (ev,inj_open_wb cb)) - (apply_with_ebindings_gen ev cb) +let h_apply simple ev cb = + abstract_tactic (TacApply (simple,ev,inj_open_wb cb)) + (apply_with_ebindings_gen simple ev cb) let h_elim ev cb cbo = abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) (elim ev cb cbo) @@ -123,8 +123,8 @@ let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c) -let h_simplest_apply c = h_apply false (c,NoBindings) -let h_simplest_eapply c = h_apply true (c,NoBindings) +let h_simplest_apply c = h_apply false false (c,NoBindings) +let h_simplest_eapply c = h_apply false true (c,NoBindings) let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) |