From 3fe5f962d236448e78f55dd6761da173a30f8be4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Nov 2020 13:38:41 +0100
Subject: Tentative fix for the refman.

---
 doc/sphinx/proofs/automatic-tactics/auto.rst | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index 485b92342d..510457fd0c 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -123,6 +123,10 @@ Programmable proof search
 
    .. example::
 
+      .. coqtop:: none
+
+         Set Warnings "-deprecated-hint-without-locality".
+
       .. coqtop:: all
 
          Hint Resolve ex_intro : core.
@@ -405,6 +409,10 @@ automatically created.
 
       .. example::
 
+         .. coqtop:: none
+
+            Set Warnings "-deprecated-hint-without-locality".
+
          .. coqtop:: in
 
             Hint Extern 4 (~(_ = _)) => discriminate : core.
@@ -419,7 +427,11 @@ automatically created.
 
       .. example::
 
-         .. coqtop:: reset all
+         .. coqtop:: reset none
+
+            Set Warnings "-deprecated-hint-without-locality".
+
+         .. coqtop:: all
 
             Require Import List.
             Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
-- 
cgit v1.2.3