From 85fe61e5d7ce550811a40ac8d9a28fffcf20fb1d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 1 Sep 2017 16:43:43 +0200
Subject: Remove unused function Evd.whd_sort_variable

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

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index b39069174..d1c7fef73 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -820,8 +820,6 @@ let fresh_constructor_instance ?loc env evd c =
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
   with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
 
-let whd_sort_variable evd t = t
-
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
 let is_flexible_level evd l = 
-- 
cgit v1.2.3