From b09444fdaee1cf608dd40465d5e400fbd46ef6ad Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 16 Sep 2019 19:19:07 -0400
Subject: Make rapply handle all numbers of underscores

Also add a tactic notation so that it takes in uconstrs by default.

Also add some basic tests for `rapply`.

Also document rapply in the manual
---
 test-suite/success/rapply.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 test-suite/success/rapply.v

(limited to 'test-suite')

diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v
new file mode 100644
index 0000000000..5bc2322842
--- /dev/null
+++ b/test-suite/success/rapply.v
@@ -0,0 +1,22 @@
+Require Import Coq.Program.Tactics.
+
+Ltac test n :=
+  (*let __ := match goal with _ => idtac n end in*)
+  lazymatch n with
+  | O => let __ := match goal with _ => assert True by rapply I; clear end in
+         uconstr:(fun _ => I)
+  | S ?n'
+    => let lem := test n' in
+       let __ := match goal with _ => assert True by (unshelve rapply lem; try exact I); clear end in
+       uconstr:(fun _ : True => lem)
+  end.
+
+Goal True.
+  assert True by rapply I.
+  assert True by (unshelve rapply (fun _ => I); try exact I).
+  assert True by (unshelve rapply (fun _ _ => I); try exact I).
+  assert True by (unshelve rapply (fun _ _ _ => I); try exact I).
+  clear.
+  Time let __ := test 50 in idtac.
+  rapply I.
+Qed.
-- 
cgit v1.2.3


From 8d9afb9c459ed7affdf6c0752ff6397e0281e0c3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 19 Sep 2019 16:31:33 -0400
Subject: Remove `rapply` tactic notation in favor of just the tactic

This increases backwards compatibility.  If desired, we can add a tactic
notation to simplify the spec of `rapply` in the future if we want.
---
 test-suite/success/rapply.v | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v
index 5bc2322842..13efd986f0 100644
--- a/test-suite/success/rapply.v
+++ b/test-suite/success/rapply.v
@@ -1,22 +1,27 @@
 Require Import Coq.Program.Tactics.
 
+(** We make a version of [rapply] that takes [uconstr]; we do not
+currently test what scope [rapply] interprets terms in. *)
+
+Tactic Notation "urapply" uconstr(p) := rapply p.
+
 Ltac test n :=
   (*let __ := match goal with _ => idtac n end in*)
   lazymatch n with
-  | O => let __ := match goal with _ => assert True by rapply I; clear end in
+  | O => let __ := match goal with _ => assert True by urapply I; clear end in
          uconstr:(fun _ => I)
   | S ?n'
     => let lem := test n' in
-       let __ := match goal with _ => assert True by (unshelve rapply lem; try exact I); clear end in
+       let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in
        uconstr:(fun _ : True => lem)
   end.
 
 Goal True.
-  assert True by rapply I.
-  assert True by (unshelve rapply (fun _ => I); try exact I).
-  assert True by (unshelve rapply (fun _ _ => I); try exact I).
-  assert True by (unshelve rapply (fun _ _ _ => I); try exact I).
+  assert True by urapply I.
+  assert True by (unshelve urapply (fun _ => I); try exact I).
+  assert True by (unshelve urapply (fun _ _ => I); try exact I).
+  assert True by (unshelve urapply (fun _ _ _ => I); try exact I).
   clear.
   Time let __ := test 50 in idtac.
-  rapply I.
+  urapply I.
 Qed.
-- 
cgit v1.2.3