From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 vernac/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/record.ml')

diff --git a/vernac/record.ml b/vernac/record.ml
index 8b4b7606fc..53722b8f61 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -216,7 +216,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then user_err ~hdr:"structure" st;
-  Flags.if_verbose Feedback.msg_info (hov 0 st)
+  warn_cannot_define_projection (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
-- 
cgit v1.2.3