From 6e5dd2ee8bc014d1f99cef3156a5114b11510398 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 17:00:10 +0200
Subject: Remove remnants of polymorphic instance name registration.

---
 engine/univNames.ml  | 2 --
 engine/univNames.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'engine')

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 5c87fed31c..b7ccd2372f 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -53,8 +53,6 @@ let compute_instance_binders inst ubinders =
   in
   Array.map_to_list map (Instance.to_array inst)
 
-let register_universe_binders ref ubinders = ()
-
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 634db9581c..b00c5fda95 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -21,8 +21,6 @@ val empty_binders : universe_binders
 
 val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
 
-val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
-
 type univ_name_list = Names.lname list
 
 (** [universe_binders_with_opt_names ref l]
-- 
cgit v1.2.3