From cea3d7c83bf3aae18262e62b897ec204c098e444 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 1 Sep 2017 16:14:03 +0200
Subject: Remove unused env argument to fresh_sort_in_family

(Universes and Evd)
---
 engine/evd.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 761ae79832..b390691742 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -805,8 +805,8 @@ let make_flexible_variable evd ~algebraic u =
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
-  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
+  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
 
 let fresh_constant_instance ?loc env evd c =
   with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
-- 
cgit v1.2.3


From 85fe61e5d7ce550811a40ac8d9a28fffcf20fb1d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
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 b390691742..d1c7fef738 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