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

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

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 816a8c4703..a4406aeba1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -29,7 +29,7 @@ open Context.Rel.Declaration
 let type_of_inductive env (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
  Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
- Inductive.type_of_inductive env (specif,u)
+ Inductive.type_of_inductive (specif,u)
 
 (* Return type as quoted by the user *)
 let type_of_constructor env (cstr,u) =
-- 
cgit v1.2.3