From 575da16f72ac125ba7e50b1bfe63302dee639973 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 May 2016 18:19:15 +0200
Subject: Adding a local type-in-type flag in kernel declarations.

---
 kernel/term_typing.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f0c116d275..a7c6ef0572 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -269,6 +269,7 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+  let flags = { flags with check_universes = flags.check_universes && not (type_in_type env) } in
   let open Context.Named.Declaration in
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
-- 
cgit v1.2.3