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.
---
 doc/sphinx/addendum/type-classes.rst |  4 ++++
 test-suite/bugs/closed/5012.v        | 17 +++++++++++++++++
 vernac/record.ml                     | 16 +++++++++++-----
 3 files changed, 32 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/bugs/closed/5012.v

diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 6c7258f9c..68b5b9d6f 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -296,6 +296,10 @@ Variants:
    This variant declares a class a posteriori from a constant or
    inductive definition. No methods or instances are defined.
 
+   .. warn:: @ident is already declared as a typeclass
+
+      This command has no effect when used on a typeclass.
+
 .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }
 
 The :cmd:`Instance` command is used to declare a type class instance named
diff --git a/test-suite/bugs/closed/5012.v b/test-suite/bugs/closed/5012.v
new file mode 100644
index 000000000..5326c0fbb
--- /dev/null
+++ b/test-suite/bugs/closed/5012.v
@@ -0,0 +1,17 @@
+Class Foo := { foo : Set }.
+
+Axiom admit : forall {T}, T.
+
+Global Instance Foo0 : Foo
+  := {| foo := admit |}.
+
+Global Instance Foo1 : Foo
+  := { foo := admit }.
+
+Existing Class Foo.
+
+Global Instance Foo2 : Foo
+  := { foo := admit }. (* Error: Unbound method name foo of class Foo. *)
+
+Set Warnings "+already-existing-class".
+Fail Existing Class Foo.
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