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

1 files changed, 22 insertions, 0 deletions

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.