diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-10 23:41:05 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-02 06:54:30 +0200 |
| commit | b0fcd54d69c2f404a17f7bbcd0426c0bac0080f7 (patch) | |
| tree | 57459c894491fea0d9d4b31c744bc704997dd822 /plugins/ltac/tacexpr.ml | |
| parent | f29f8f80c8ad94576c7a36f3f638866c208338a0 (diff) | |
[api] Move some types to their proper module.
We solve some modularity and type duplication problems by moving types
to a better place. In particular:
- We move tactics types from `Misctypes` to `Tactics` as this is their
proper module an single user [with LTAC].
- We deprecate aliases in `Tacexpr` to such tactic types.
cc: #6512
Diffstat (limited to 'plugins/ltac/tacexpr.ml')
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8b0c44041..3baa475ab 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector = | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,7 +73,7 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * + 'dconstr with_bindings Tactics.destruction_arg * (intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -265,7 +269,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) |