diff options
Diffstat (limited to 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 25 |
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) |