diff options
| author | Pierre-Marie Pédrot | 2017-08-04 13:04:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-04 14:14:46 +0200 |
| commit | fce4a1a9cbb57a636155181898ae4ecece5af59d (patch) | |
| tree | 62777a8c6e2a389f45a174046858233f01ab34e4 /src/tac2tactics.ml | |
| parent | b84b03bb6230fca69cd9191ba0424402a5cd2330 (diff) | |
Adding the induction and destruct tactics.
Diffstat (limited to 'src/tac2tactics.ml')
| -rw-r--r-- | src/tac2tactics.ml | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index 2590d7daed..439250db78 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -6,7 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Misctypes +open Tactypes open Tactics +open Proofview open Tacmach.New open Tacticals.New open Proofview.Notations @@ -23,3 +26,21 @@ let apply adv ev cb cl = match cl with | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl + +type induction_clause = + EConstr.constr with_bindings tactic destruction_arg * + intro_pattern_naming option * + or_and_intro_pattern option * + Locus.clause option + +let map_destruction_arg = function +| ElimOnConstr c -> ElimOnConstr (delayed_of_tactic c) +| ElimOnIdent id -> ElimOnIdent id +| ElimOnAnonHyp n -> ElimOnAnonHyp n + +let map_induction_clause ((clear, arg), eqn, as_, occ) = + ((clear, map_destruction_arg arg), (eqn, as_), occ) + +let induction_destruct isrec ev ic using = + let ic = List.map map_induction_clause ic in + Tactics.induction_destruct isrec ev (ic, using) |