From 49d21a292c3a57e8ec01888745957716834f1e36 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 16 Sep 2019 19:18:57 -0400
Subject: Remove some trailing whitespace in theories/Program/Tactics.v

---
 theories/Program/Tactics.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index ba8e4dff6d..51c7fe81b9 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -61,12 +61,12 @@ Ltac destruct_pairs := repeat (destruct_one_pair).
 
 Ltac destruct_one_ex :=
   let tac H := let ph := fresh "H" in (destruct H as [H ph]) in
-  let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in 
-    (destruct H as [H ph ph']) 
+  let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in
+    (destruct H as [H ph ph'])
   in
   let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in
-  let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in 
-    (destruct H as [H ph ph']) 
+  let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in
+    (destruct H as [H ph ph'])
   in
     match goal with
       | [H : (ex _) |- _] => tac H
@@ -140,7 +140,7 @@ Ltac clear_dups := repeat clear_dup.
 
 (** Try to clear everything except some hyp *)
 
-Ltac clear_except hyp := 
+Ltac clear_except hyp :=
   repeat match goal with [ H : _ |- _ ] =>
            match H with
              | hyp => fail 1
-- 
cgit v1.2.3


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


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

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 06fc2f73b2..c8a100b0e7 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -178,9 +178,6 @@ Ltac rapply p :=
    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. *)
 
 Ltac on_call f tac :=
-- 
cgit v1.2.3