From faef5dcc656148273063f25716923d9bd1fe2497 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 9 Feb 2020 19:49:33 +0100
Subject: Use thunks to univ instead of lazy constr for template typing

---
 kernel/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 3771454db5..b6b8e5265c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -158,7 +158,7 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
 let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let auxntyp = 1 in
   let specif = (lookup_mind_specif env mi, u) in
-  let ty = type_of_inductive env specif in
+  let ty = type_of_inductive specif in
   let env' =
     let r = (snd (fst specif)).mind_relevance in
     let anon = Context.make_annot Anonymous r in
-- 
cgit v1.2.3