From 85a4780bcb462a9fb5a86bb510929e036171d2fe Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Jul 2020 19:01:43 +0200
Subject: Tweak the warning for arbitrary term hints.

Fixes #11970.
---
 vernac/comHints.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index b05bf9a675..0e3e3c61a9 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -64,11 +64,11 @@ let project_hint ~poly pri l2r r =
   (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
 
 let warn_deprecated_hint_constr =
-  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+  CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
     (fun () ->
       Pp.strbrk
-        "Declaring arbitrary terms as hints is deprecated; declare a global \
-         reference instead")
+        "Declaring arbitrary terms as hints is fragile; it is recommended to \
+         declare a toplevel constant instead")
 
 let interp_hints ~poly h =
   let env = Global.env () in
-- 
cgit v1.2.3


From de89e569c1816e9b2ea5b0ad30b03d18bd71fd64 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Jul 2020 19:04:37 +0200
Subject: Add changelog.

---
 .../07-commands-and-options/12678-tweak-hint-constr-warning.rst     | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst

diff --git a/doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst b/doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst
new file mode 100644
index 0000000000..9de072060d
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Arbitrary hints have been undeprecated, and their definition
+  now triggers a standard warning instead
+  (`#12678 <https://github.com/coq/coq/pull/12678>`_,
+  fixes `#11970 <https://github.com/coq/coq/issues/11970>`_,
+  by Pierre-Marie Pédrot).
-- 
cgit v1.2.3


From f41fccaaf30ea4f76edb8204fa5f4022467b6e0c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 10 Jul 2020 23:29:05 +0200
Subject: Remove automatic formatting of ComHints.

This is about the third time I try to kill this file but for some reason
it is still here.
---
 vernac/.ocamlformat-enable | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 vernac/.ocamlformat-enable

diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable
deleted file mode 100644
index ffaa7e70f4..0000000000
--- a/vernac/.ocamlformat-enable
+++ /dev/null
@@ -1 +0,0 @@
-comHints.ml
-- 
cgit v1.2.3