From 3f734c5f5338feb491a6ca021e8b5a578f95c88b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 26 Sep 2017 17:52:34 +0200
Subject: Slightly more straightforward notation for (e)apply.

---
 tests/example2.v     |  7 +++++++
 theories/Notations.v | 16 ++--------------
 2 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/tests/example2.v b/tests/example2.v
index a21f3a7f4e..378abb86a8 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -44,6 +44,13 @@ apply &H with (m := 0).
 split.
 Qed.
 
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> (0 = 1) -> P 0.
+Proof.
+intros P H e.
+apply &H with (m := 1) in e.
+exact e.
+Qed.
+
 Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
 Proof.
 intros P H.
diff --git a/theories/Notations.v b/theories/Notations.v
index 1b5792e051..d4520dbdfd 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -246,28 +246,16 @@ Ltac2 Notation "eelim" c(thunk(constr)) bnd(thunk(with_bindings))
   elim0 true c bnd use.
 
 Ltac2 apply0 adv ev cb cl :=
-  let cl := match cl with
-  | None => None
-  | Some p =>
-    let ((_, id, ipat)) := p in
-    let p := match ipat with
-    | None => None
-    | Some p =>
-      let ((_, ipat)) := p in
-      Some ipat
-    end in
-    Some (id, p)
-  end in
   Std.apply adv ev cb cl.
 
 Ltac2 Notation "eapply"
   cb(list1(thunk(seq(constr, with_bindings)), ","))
-  cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
+  cl(opt(seq("in", ident, opt(seq("as", intropattern))))) :=
   apply0 true true cb cl.
 
 Ltac2 Notation "apply"
   cb(list1(thunk(seq(constr, with_bindings)), ","))
-  cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
+  cl(opt(seq("in", ident, opt(seq("as", intropattern))))) :=
   apply0 true false cb cl.
 
 Ltac2 default_on_concl cl :=
-- 
cgit v1.2.3