diff options
| -rw-r--r-- | theories/Notations.v | 20 |
1 files changed, 6 insertions, 14 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 0487e324ca..2d7b4c8a8b 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -36,28 +36,20 @@ Ltac2 Notation "econstructor" := Std.constructor true. Ltac2 Notation "econstructor" n(tactic) bnd(bindings) := Std.constructor_n true n bnd. -Ltac2 eelim c bnd use := +Ltac2 elim0 ev c bnd use := let use := match use with | None => None | Some u => let ((_, c, wth)) := u in Some (c, wth) end in - Std.elim true (c, bnd) use. + Std.elim ev (c, bnd) use. -Ltac2 elim c bnd use := +Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings)) + use(thunk(opt(seq("using", constr, bindings)))) := 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 false (c, bnd) use). - -Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings)) - use(thunk(opt(seq("using", constr, bindings)))) := elim c bnd use. + (fun ((c, bnd, use)) => elim0 false c bnd use). Ltac2 Notation "eelim" c(constr) bnd(bindings) use(opt(seq("using", constr, bindings))) := - eelim c bnd use. + elim0 true c bnd use. |