diff options
| author | Hugo Herbelin | 2016-01-21 01:43:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-01-21 09:29:26 +0100 |
| commit | 9c2662eecc398f38be3b6280a8f760cc439bc31c (patch) | |
| tree | 497b1c250e3cb2e918982b25bb029c14603ac96f /intf | |
| parent | 4b075af747f65bcd73ff1c78417cf77edf6fbd76 (diff) | |
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 65c7dccf2a..889dc54448 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -16,6 +16,8 @@ type patvar = Id.t (** Introduction patterns *) +type tuple_flag = bool (* tells pattern list should be list of fixed length *) + type 'constr intro_pattern_expr = | IntroForthcoming of bool | IntroNaming of intro_pattern_naming_expr @@ -31,7 +33,8 @@ and 'constr intro_pattern_action_expr = | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = - (Loc.t * 'constr intro_pattern_expr) list list + | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list + | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list (** Move destination for hypothesis *) |