summaryrefslogtreecommitdiff
path: root/tactics/hiddentac.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /tactics/hiddentac.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'tactics/hiddentac.ml')
-rw-r--r--tactics/hiddentac.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 1fe1c51e..76014955 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hiddentac.ml 7875 2006-01-16 09:55:24Z herbelin $ *)
+(* $Id: hiddentac.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
open Term
open Proof_type
@@ -23,7 +23,7 @@ let inj_id id = (dummy_loc,id)
(* Basic tactics *)
let h_intro_move x y =
- abstract_tactic (TacIntroMove (x, option_app inj_id y)) (intro_move x y)
+ abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y)
let h_intro x = h_intro_move (Some x) None
let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
let h_assumption = abstract_tactic TacAssumption assumption
@@ -88,7 +88,9 @@ let h_simplest_right = h_right NoBindings
(* Conversion *)
let h_reduce r cl = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
-let h_change oc c cl = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl)
+let h_change oc c cl =
+ abstract_tactic (TacChange (oc,c,cl))
+ (change (option_map Redexpr.out_with_occurrences oc) c cl)
(* Equivalence relations *)
let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity