From d180279aa934dfbb3fd97e707675b55f464f14ef Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 6 Oct 2016 14:02:52 +0200
Subject: Disable compatibility notations warnings.

Enablnig them would give a system that tells the user to replace e.g.:

le_n_Sn with Nat.le_succ_diag_r
lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same
lemma is called lt_lt_succ)

In many cases, the new names will be too painful for intensive users.
---
 interp/syntax_def.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index b2b82cce37..2523063e64 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -93,8 +93,8 @@ let pr_compat_warning (kn, def, v) =
   pr_syndef kn ++ pp_def ++ since
 
 let warn_compatibility_notation =
-  CWarnings.create ~name:"compatibility-notation"
-                   ~category:"deprecated" pr_compat_warning
+  CWarnings.(create ~name:"compatibility-notation"
+                    ~category:"deprecated" ~default:Disabled pr_compat_warning)
 
 let verbose_compat kn def = function
   | Some v when Flags.version_strictly_greater v ->
-- 
cgit v1.2.3