Imported Upstream version 8.4dfsgupstream/8.4dfsg

1 files changed, 14 insertions, 11 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index fafc681a..87f19105 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -61,12 +61,15 @@ let h_generalize cl =
     cl)
 let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep 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,c,cl,b)) (letin_tac with_eq na c None cl)
-let h_let_pat_tac b na c cl =
-  let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
-  abstract_tactic (TacLetTac (na,snd c,cl,b))
+let h_let_tac b na c cl eqpat =
+  let id = Option.default (dummy_loc,IntroAnonymous) eqpat in
+  let with_eq = if b then None else Some (true,id) in
+  abstract_tactic (TacLetTac (na,c,cl,b,eqpat))
+    (letin_tac with_eq na c None cl)
+let h_let_pat_tac b na c cl eqpat =
+  let id = Option.default (dummy_loc,IntroAnonymous) eqpat in
+  let with_eq = if b then None else Some (true,id) in
+  abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat))
     (letin_pat_tac with_eq na c None cl)
 
 (* Derived basic tactics *)
@@ -82,12 +85,12 @@ let out_indarg = function
   | ElimOnAnonHyp n -> ElimOnAnonHyp n
 
 let h_induction_destruct isrec ev lcl =
-  let lcl' = on_fst (List.map (fun (a,b,c) ->(List.map out_indarg a,b,c))) lcl in
+  let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in
   abstract_tactic (TacInductionDestruct (isrec,ev,lcl'))
     (induction_destruct isrec ev lcl)
-let h_new_induction ev c e idl cl =
-  h_induction_destruct true ev ([c,e,idl],cl)
-let h_new_destruct ev c e idl cl = h_induction_destruct false ev ([c,e,idl],cl)
+let h_new_induction ev c idl e cl =
+  h_induction_destruct true ev ([c,idl],e,cl)
+let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl)
 
 let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d)
 let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)