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
---
 doc/sphinx/proof-engine/tactics.rst | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4f903d5776..843a8933be 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -685,6 +685,22 @@ Applying theorems
       instantiate (see :ref:`Existential-Variables`). The instantiation is
       intended to be found later in the proof.
 
+   .. tacv:: rapply @term
+      :name: rapply
+
+      The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it
+      uses the proof engine of :tacn:`refine` for dealing with
+      existential variables, holes, and conversion problems.  This may
+      result in slightly different behavior regarding which conversion
+      problems are solvable.  Note that :tacn:`rapply` prefers to
+      instantiate as many hypotheses of :n:`@term` as possible.  As a
+      result, if it is possible to apply :n:`@term` to arbitrarily
+      many arguments without getting a type error, :tacn:`rapply` will
+      loop.
+
+      Note that you need to :n:`Require Import Coq.Program.Tactics` to
+      make use of :tacn:`rapply`.
+
    .. tacv:: simple apply @term.
 
       This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms
-- 
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.
---
 doc/sphinx/proof-engine/tactics.rst | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 843a8933be..3994ff411c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -692,11 +692,17 @@ Applying theorems
       uses the proof engine of :tacn:`refine` for dealing with
       existential variables, holes, and conversion problems.  This may
       result in slightly different behavior regarding which conversion
-      problems are solvable.  Note that :tacn:`rapply` prefers to
-      instantiate as many hypotheses of :n:`@term` as possible.  As a
-      result, if it is possible to apply :n:`@term` to arbitrarily
-      many arguments without getting a type error, :tacn:`rapply` will
-      loop.
+      problems are solvable.  However, like :tacn:`apply` but unlike
+      :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes
+      which remain in :n:`@term` itself after typechecking and
+      typeclass resolution but before unification with the goal.  More
+      technically, :n:`@term` is first parsed as a
+      :production:`constr` rather than as a :production:`uconstr` or
+      :production:`open_constr` before being applied to the goal. Note
+      that :tacn:`rapply` prefers to instantiate as many hypotheses of
+      :n:`@term` as possible.  As a result, if it is possible to apply
+      :n:`@term` to arbitrarily many arguments without getting a type
+      error, :tacn:`rapply` will loop.
 
       Note that you need to :n:`Require Import Coq.Program.Tactics` to
       make use of :tacn:`rapply`.
-- 
cgit v1.2.3