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)
---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/inv.ml')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index e467eacd97..43786c8e19 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -94,7 +94,7 @@ let make_inv_predicate env evd indf realargs id status concl =
               | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
               | None ->
 		let sort = get_sort_family_of env !evd concl in
-		let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in
+                let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in
 		let p = make_arity env !evd true indf sort in
 		let evd',(p,ptyp) = Unification.abstract_list_all env
                   !evd p concl (realargs@[mkVar id])
-- 
cgit v1.2.3