From 6d416ea54fd26987188858bcf80461247b002a09 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 21 Mar 2017 14:30:58 +0100 Subject: Add a few comments in term_typing.ml. --- kernel/term_typing.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2d5580347..b7597ba7f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -164,6 +164,10 @@ let infer_declaration ~trust env kn dcl = let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in Undef nl, RegularArity t, None, poly, univs, false, ctx + (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, + so we delay the typing and hash consing of its body. + Remark: when the universe quantification is given explicitly, we could + delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_polymorphic = false} as c) -> @@ -192,6 +196,7 @@ let infer_declaration ~trust env kn dcl = c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx + (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in -- cgit v1.2.3