diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-21 14:30:58 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-21 17:15:27 +0100 |
| commit | 6d416ea54fd26987188858bcf80461247b002a09 (patch) | |
| tree | 0f11ea63c8312523d2a91805a4b0f331fdd78f4f /kernel | |
| parent | 09c856a3bcb7369244202ed94db247f7abe84dad (diff) | |
Add a few comments in term_typing.ml.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |