From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 21 Sep 2017 11:14:11 +0200
Subject: Forbid repeated names in universe binders.

---
 engine/evd.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 9ea2cc00f..0f17e0dc6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -935,9 +935,6 @@ let nf_constraints evd =
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s
 
-let add_universe_name evd s l =
-  { evd with universes = UState.add_universe_name evd.universes s l }
-
 let universe_binders evd = UState.universe_binders evd.universes
 
 let universes evd = UState.ugraph evd.universes
-- 
cgit v1.2.3