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/univGen.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/univGen.ml') diff --git a/engine/univGen.ml b/engine/univGen.ml index 796a1bcc1..b07d4848f 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -215,7 +215,7 @@ let type_of_reference env r = let type_of_global t = type_of_reference (Global.env ()) t -let fresh_sort_in_family env = function +let fresh_sort_in_family = function | InProp -> Sorts.prop, ContextSet.empty | InSet -> Sorts.set, ContextSet.empty | InType -> @@ -223,7 +223,7 @@ let fresh_sort_in_family env = function Type (Univ.Universe.make u), ContextSet.singleton u let new_sort_in_family sf = - fst (fresh_sort_in_family (Global.env ()) sf) + fst (fresh_sort_in_family sf) let extend_context (a, ctx) (ctx') = (a, ContextSet.union ctx ctx') -- cgit v1.2.3