Merge PR #10760: Make rapply handle all numbers of underscores

Ack-by: Zimmi48
Reviewed-by: ppedrot

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v
new file mode 100644
index 0000000000..13efd986f0
--- /dev/null
+++ b/test-suite/success/rapply.v
@@ -0,0 +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 urapply I; clear end in
+         uconstr:(fun _ => I)
+  | S ?n'
+    => let lem := test n' 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 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.
+  urapply I.
+Qed.