diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 26 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
2 files changed, 28 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index d0400667db..ec7a6b0b12 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -35,3 +35,29 @@ Ltac2 Notation "constructor" n(tactic) bnd(thunk(bindings)) := Ltac2 Notation "econstructor" := Std.econstructor (). Ltac2 Notation "econstructor" n(tactic) bnd(bindings) := Std.econstructor_n n bnd. + +Ltac2 eelim c bnd use := + let use := match use with + | None => None + | Some u => + let ((_, c, wth)) := u in Some (c, wth) + end in + Std.eelim (c, bnd) use. + +Ltac2 elim c bnd use := + Control.with_holes + (fun () => c (), bnd (), use ()) + (fun ((c, bnd, use)) => + let use := match use with + | None => None + | Some u => + let ((_, c, wth)) := u in Some (c, wth) + end in + Std.elim (c, bnd) use). + +Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings)) + use(thunk(opt(seq("using", constr, bindings)))) := elim c bnd use. + +Ltac2 Notation "eelim" c(constr) bnd(bindings) + use(opt(seq("using", constr, bindings))) := + eelim c bnd use. diff --git a/theories/Std.v b/theories/Std.v index d2b85f215e..3d0f463c5e 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -78,7 +78,9 @@ with or_and_intro_pattern := [ Ltac2 @ external intros : intro_pattern list -> unit := "ltac2" "tac_intros". Ltac2 @ external eintros : intro_pattern list -> unit := "ltac2" "tac_eintros". +Ltac2 @ external elim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim". Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim". +Ltac2 @ external case : constr_with_bindings -> unit := "ltac2" "tac_case". Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase". Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize". |