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