summaryrefslogtreecommitdiff
path: root/tactics/hiddentac.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-01 17:21:14 +0200
commitda178a880e3ace820b41d38b191d3785b82991f5 (patch)
tree6356ab3164a5ad629f4161dc6c44ead74edc2937 /tactics/hiddentac.ml
parente4282ea99c664d8d58067bee199cbbcf881b60d5 (diff)
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
Diffstat (limited to 'tactics/hiddentac.ml')
-rw-r--r--tactics/hiddentac.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 8e517453..4ab40acb 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *)
+(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *)
open Term
open Proof_type
@@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h =
let h_simple_induction = h_simple_induction_destruct true
let h_simple_destruct = h_simple_induction_destruct false
-let h_induction_destruct isrec ev l =
+let h_induction_destruct ev isrec l =
abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) ->
List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l))
- (induction_destruct ev isrec l)
+ (induction_destruct isrec ev l)
let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl]
let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl]
@@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l)
(* Constructors *)
let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l)
-let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l)
+let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l)
let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l)
(* Moved to tacinterp because of dependencies in Tacinterp.interp
let h_any_constructor t =