From 70e01149ad4c74d086f042f0cced74b1d0e228bf Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Sat, 27 Apr 2019 16:11:05 +0200
Subject: Document _no_check tactics (#3225)

Triggered by trying to understand https://gitlab.mpi-sws.org/iris/iris/merge_requests/235.

- Add a new section at the end
- Document change_no_check, and convert_concl_no_check, address review comments
---
 doc/sphinx/proof-engine/tactics.rst | 80 +++++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8d9e99b9d5..02a0867341 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4811,3 +4811,83 @@ references to automatically generated names.
    :name: Mangle Names Prefix
 
    Specifies the prefix to use when generating names.
+
+Performance-oriented tactic variants
+------------------------------------
+
+.. tacn:: change_no_check @term
+   :name: change_no_check
+
+   For advanced usage. Similar to :n:`change @term`, but as an optimization,
+   it skips checking that :n:`@term` is convertible to the goal.
+
+   Recall the Coq kernel typechecks proofs again when they are concluded to
+   ensure safety. Hence, using :tacn:`change` checks convertibility twice
+   overall, while :tacn:`convert_concl_no_check` can produce ill-typed terms,
+   but checks convertibility only once.
+   Hence, :tacn:`convert_concl_no_check` can be useful to speed up certain proof
+   scripts, especially if one knows by construction that the argument is
+   indeed convertible to the goal.
+
+   In the following example, :tacn:`convert_concl_no_check` replaces :g:`False` by
+   :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency.
+
+   .. example::
+
+      .. coqtop:: all abort
+
+         Goal False.
+           change_no_check True.
+           exact I.
+         Fail Qed.
+
+   .. tacv:: convert_concl_no_check @term
+      :name: convert_concl_no_check
+
+      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
+      variants.
+
+.. tacn:: exact_no_check @term
+   :name: exact_no_check
+
+   For advanced usage. Similar to :n:`exact @term`, but as an optimization,
+   it skips checking that :n:`@term` has the goal's type, relying on the kernel
+   check instead. See :tacn:`convert_concl_no_check` for more explanations.
+
+   .. example::
+
+      .. coqtop:: all abort
+
+         Goal False.
+           exact_no_check I.
+         Fail Qed.
+
+   .. tacv:: vm_cast_no_check @term
+      :name: vm_cast_no_check
+
+      For advanced usage. Similar to :n:`exact_no_check @term`, but additionally
+      instructs the kernel to use :tacn:`vm_compute` to compare the
+      goal's type with the :n:`@term`'s type.
+
+      .. example::
+
+        .. coqtop:: all abort
+
+            Goal False.
+              vm_cast_no_check I.
+            Fail Qed.
+
+   .. tacv:: native_cast_no_check @term
+      :name: native_cast_no_check
+
+      for advanced usage. similar to :n:`exact_no_check @term`, but additionally
+      instructs the kernel to use :tacn:`native_compute` to compare the goal's
+      type with the :n:`@term`'s type.
+
+      .. example::
+
+        .. coqtop:: all abort
+
+            Goal False.
+              native_cast_no_check I.
+            Fail Qed.
-- 
cgit v1.2.3


From f247ae382ccf7a292f15195646ff7302a7c2bd69 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 3 May 2019 03:27:05 +0200
Subject: Copy-editing from code review

Co-Authored-By: Blaisorblade <p.giarrusso@gmail.com>---
 doc/sphinx/proof-engine/tactics.rst | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 02a0867341..1f339e7761 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4821,15 +4821,15 @@ Performance-oriented tactic variants
    For advanced usage. Similar to :n:`change @term`, but as an optimization,
    it skips checking that :n:`@term` is convertible to the goal.
 
-   Recall the Coq kernel typechecks proofs again when they are concluded to
+   Recall that the Coq kernel typechecks proofs again when they are concluded to
    ensure safety. Hence, using :tacn:`change` checks convertibility twice
-   overall, while :tacn:`convert_concl_no_check` can produce ill-typed terms,
+   overall, while :tacn:`change_no_check` can produce ill-typed terms,
    but checks convertibility only once.
-   Hence, :tacn:`convert_concl_no_check` can be useful to speed up certain proof
+   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
    scripts, especially if one knows by construction that the argument is
    indeed convertible to the goal.
 
-   In the following example, :tacn:`convert_concl_no_check` replaces :g:`False` by
+   In the following example, :tacn:`change_no_check` replaces :g:`False` by
    :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency.
 
    .. example::
@@ -4852,7 +4852,7 @@ Performance-oriented tactic variants
 
    For advanced usage. Similar to :n:`exact @term`, but as an optimization,
    it skips checking that :n:`@term` has the goal's type, relying on the kernel
-   check instead. See :tacn:`convert_concl_no_check` for more explanations.
+   check instead. See :tacn:`change_no_check` for more explanations.
 
    .. example::
 
-- 
cgit v1.2.3