From 9b142e358daf798cab79cafba6d9da5941481f53 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Dec 2018 19:54:19 +0100
Subject: Remove useless freshness check in new_instance

---
 vernac/classes.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 7c79c46fe2..6c44745c81 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -105,8 +105,6 @@ let id_of_class cl =
 	  mip.(0).Declarations.mind_typename
     | _ -> assert false
 
-open Pp
-
 let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
   let info = intern_info info in
@@ -330,11 +328,7 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
   in
   let id =
     match instid with
-      Name id ->
-      let sp = Lib.make_path id in
-      if Nametab.exists_cci sp then
-        user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
-      id
+    | Name id -> id
     | Anonymous ->
       let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
       Namegen.next_global_ident_away i (Termops.vars_of_env env)
-- 
cgit v1.2.3