diff options
| author | Pierre-Marie Pédrot | 2017-08-01 16:56:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-01 19:39:29 +0200 |
| commit | c3be78f96b91a042944f9bee66bf0ea8d929a37d (patch) | |
| tree | 4122408124a9b04c3e7f8e08f1c3304792391483 /theories | |
| parent | 30fc910b01f61ce3691ed63a0908c1c60cee76dd (diff) | |
Introducing the all-mighty intro-patterns.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Std.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/theories/Std.v b/theories/Std.v index 3070c2e005..a27790c35d 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -49,8 +49,35 @@ Ltac2 Type red_flags := { rConst : evaluable_reference list }. +Ltac2 Type 'a not_implemented. + +Ltac2 Type rec intro_pattern := [ +| IntroForthcoming (bool) +| IntroNaming (intro_pattern_naming) +| IntroAction (intro_pattern_action) +] +with intro_pattern_naming := [ +| IntroIdentifier (ident) +| IntroFresh (ident) +| IntroAnonymous +] +with intro_pattern_action := [ +| IntroWildcard +| IntroOrAndPattern (or_and_intro_pattern) +| IntroInjection (intro_pattern list) +| IntroApplyOn ((constr * intro_pattern) not_implemented) (* Not Implemented yet *) +| IntroRewrite (bool) +] +with or_and_intro_pattern := [ +| IntroOrPattern (intro_pattern list list) +| IntroAndPattern (intro_pattern list) +]. + (** Standard, built-in tactics. See Ltac1 for documentation. *) +Ltac2 @ external intros : intro_pattern list -> unit := "ltac2" "tac_intros". +Ltac2 @ external eintros : intro_pattern list -> unit := "ltac2" "tac_eintros". + Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim". Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase". |