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
---
 theories/Program/Tactics.v | 23 +++++++----------------
 1 file changed, 7 insertions(+), 16 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 51c7fe81b9..06fc2f73b2 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -173,22 +173,13 @@ Ltac on_application f tac T :=
 (** A variant of [apply] using [refine], doing as much conversion as necessary. *)
 
 Ltac rapply p :=
-  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _ _) ||
-  refine (p _ _ _ _ _) ||
-  refine (p _ _ _ _) ||
-  refine (p _ _ _) ||
-  refine (p _ _) ||
-  refine (p _) ||
-  refine p.
+  (** before we try to add more underscores, first ensure that adding such underscores is valid *)
+  (assert_succeeds (idtac; let __ := open_constr:(p _) in idtac);
+   rapply uconstr:(p _))
+  || refine p.
+
+(** The tactic [rapply] is a tactic notation so that it takes in uconstrs by default *)
+Tactic Notation "rapply" uconstr(p) := rapply p.
 
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 
-- 
cgit v1.2.3