diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.mli | 12 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 10 |
2 files changed, 13 insertions, 9 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 6ee44215c0..3d9a344ee9 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -17,14 +17,18 @@ type patvar = Id.t (** Introduction patterns *) type intro_pattern_expr = - | IntroOrAndPattern of or_and_intro_pattern_expr - | IntroInjection of (Loc.t * intro_pattern_expr) list + | IntroForthcoming of bool + | IntroNaming of intro_pattern_naming_expr + | IntroAction of intro_pattern_action_expr +and intro_pattern_naming_expr = | IntroWildcard - | IntroRewrite of bool | IntroIdentifier of Id.t | IntroFresh of Id.t - | IntroForthcoming of bool | IntroAnonymous +and intro_pattern_action_expr = + | IntroOrAndPattern of or_and_intro_pattern_expr + | IntroInjection of (Loc.t * intro_pattern_expr) list + | IntroRewrite of bool and or_and_intro_pattern_expr = (Loc.t * intro_pattern_expr) list list (** Move destination for hypothesis *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index cf8d34d7e7..2af77eb103 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -44,9 +44,9 @@ type inversion_kind = type ('c,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * intro_pattern_expr located option + inversion_kind * 'id list * or_and_intro_pattern_expr located option | DepInversion of - inversion_kind * 'c option * intro_pattern_expr located option + inversion_kind * 'c option * or_and_intro_pattern_expr located option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -58,8 +58,8 @@ type 'id message_token = type 'constr induction_clause = 'constr with_bindings induction_arg * - (intro_pattern_expr located option (* eqn:... *) - * intro_pattern_expr located option) (* as ... *) + (intro_pattern_naming_expr located option (* eqn:... *) + * or_and_intro_pattern_expr located option) (* as ... *) type ('constr,'id) induction_clause_list = 'constr induction_clause list @@ -127,7 +127,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacGeneralize of ('trm with_occurrences * Name.t) list | TacGeneralizeDep of 'trm | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * - intro_pattern_expr located option + intro_pattern_naming_expr located option (* Derived basic tactics *) | TacInductionDestruct of |