From 543e4fad4257da71bc7457da47b35d4803761118 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Oct 2018 11:54:02 +0000
Subject: [Manual] Prevent an irrelevant warning to show up

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 6fde52f95e..3ca0ffe678 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3554,6 +3554,7 @@ corresponding new goals will be generated.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
+     Set Warnings "-notation-overridden".
 
   .. coqtop:: all
 
-- 
cgit v1.2.3