diff options
| author | Maxime Dénès | 2018-12-21 19:54:19 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-22 11:17:58 +0100 |
| commit | 9b142e358daf798cab79cafba6d9da5941481f53 (patch) | |
| tree | 0c3d42f9307de5473c7622b29103cdd1ddfc4382 | |
| parent | e195c1dd97116961e34f3fad41a697a01d505ebf (diff) | |
Remove useless freshness check in new_instance
| -rw-r--r-- | vernac/classes.ml | 8 |
1 files changed, 1 insertions, 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) |