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.mli | |
| parent | b84b03bb6230fca69cd9191ba0424402a5cd2330 (diff) | |
Adding the induction and destruct tactics.
Diffstat (limited to 'src/tac2tactics.mli')
| -rw-r--r-- | src/tac2tactics.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index 86278f177e..f29793411a 100644 --- a/src/tac2tactics.mli +++ b/src/tac2tactics.mli @@ -16,3 +16,12 @@ open Proofview val apply : advanced_flag -> evars_flag -> EConstr.constr with_bindings tactic list -> (Id.t * intro_pattern option) option -> unit tactic + +type induction_clause = + EConstr.constr with_bindings tactic destruction_arg * + intro_pattern_naming option * + or_and_intro_pattern option * + Locus.clause option + +val induction_destruct : rec_flag -> evars_flag -> + induction_clause list -> EConstr.constr with_bindings option -> unit Proofview.tactic |