From 590ee35546f3528ac7ccb32306fb86e78fdce93b Mon Sep 17 00:00:00 2001
From: Paolo G. Giarrusso
Date: Fri, 3 May 2019 01:13:48 +0200
Subject: Documentation for change_no_check untested variants

Copy change's variants in change_no_check, since supposedly they should all be
supported. But they haven't been tested, and my example fails.
---
 doc/sphinx/proof-engine/tactics.rst | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 02a0867341..bb7cac17b0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4841,6 +4841,26 @@ Performance-oriented tactic variants
            exact I.
          Fail Qed.
 
+   :tacn:`change_no_check` supports all of `change`'s variants.
+
+   .. tacv:: change_no_check @term with @term’
+      :undocumented:
+
+   .. tacv:: change_no_check @term at {+ @num} with @term’
+      :undocumented:
+
+   .. tacv:: change_no_check @term {? {? at {+ @num}} with @term} in @ident
+
+      .. example::
+
+         .. coqtop:: all abort
+
+            Goal True -> False.
+              intro H.
+              change_no_check False in H.
+              exact H.
+            Fail Qed.
+
    .. tacv:: convert_concl_no_check @term
       :name: convert_concl_no_check
 
-- 
cgit v1.2.3