From c15880e6fe79f1d746f47deb22549518f1333c8a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 20 May 2018 21:21:43 +0200
Subject: Existing Class noop when already a class + warning.

Fix #5012.
---
 vernac/record.ml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index e6a3afe4e..8b665d1c5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -562,12 +562,18 @@ let add_inductive_class ind =
 	cl_unique = !typeclasses_unique }
   in add_class k
 
+let warn_already_existing_class =
+  CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g ->
+      Printer.pr_global g ++ str " is already declared as a typeclass.")
+
 let declare_existing_class g =
-  match g with
-  | ConstRef x -> add_constant_class x
-  | IndRef x -> add_inductive_class x
-  | _ -> user_err ~hdr:"declare_existing_class"
-		      (Pp.str"Unsupported class type, only constants and inductives are allowed")
+  if Typeclasses.is_class g then warn_already_existing_class g
+  else
+    match g with
+    | ConstRef x -> add_constant_class x
+    | IndRef x -> add_inductive_class x
+    | _ -> user_err ~hdr:"declare_existing_class"
+             (Pp.str"Unsupported class type, only constants and inductives are allowed")
 
 open Vernacexpr
 
-- 
cgit v1.2.3