summaryrefslogtreecommitdiff
path: root/tactics/hiddentac.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /tactics/hiddentac.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'tactics/hiddentac.ml')
-rw-r--r--tactics/hiddentac.ml15
1 files changed, 9 insertions, 6 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 31c1b02f..b270ba2d 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hiddentac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: hiddentac.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
open Term
open Proof_type
@@ -39,9 +39,12 @@ 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 simple ev cb =
- abstract_tactic (TacApply (simple,ev,List.map inj_open_wb cb))
+let h_apply simple ev cb =
+ abstract_tactic (TacApply (simple,ev,cb,None))
(apply_with_ebindings_gen simple ev cb)
+let h_apply_in simple ev cb (id,ipat as inhyp) =
+ abstract_tactic (TacApply (simple,ev,cb,Some inhyp))
+ (apply_in simple ev id cb ipat)
let h_elim ev cb cbo =
abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo))
(elim ev cb cbo)
@@ -71,7 +74,7 @@ let h_generalize_dep c =
abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c)
let h_let_tac b na c cl =
let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
- abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c cl)
+ abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
let h_instantiate n c ido =
(Evar_tactics.instantiate n c ido)
(* abstract_tactic (TacInstantiate (n,c,cls))
@@ -131,8 +134,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 false [c,NoBindings]
-let h_simplest_eapply c = h_apply false true [c,NoBindings]
+let h_simplest_apply c = h_apply false false [inj_open c,NoBindings]
+let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
let h_simplest_elim c = h_elim false (c,NoBindings) None
let h_simplest_case c = h_case false (c,NoBindings)