From 24d0027f0344bca7abce3b8fa8c2a1e42ecf1a00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 13 Sep 2014 10:44:40 +0200
Subject: Providing a -type-in-type option for collapsing the universe
 hierarchy.

---
 pretyping/indrec.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/indrec.ml')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0cbfa7597..9f460d08f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -517,7 +517,7 @@ let weaken_sort_scheme env evd set sort npars term ty =
       | Prod (n,t,c) ->
 	  if Int.equal np 0 then
             let osort, t' = change_sort_arity sort t in
-	      evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) !evdref sort osort;
+	      evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort env) !evdref sort osort;
               mkProd (n, t', c),
               mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
 	  else
-- 
cgit v1.2.3