diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 10 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 13 |
3 files changed, 15 insertions, 10 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index de1ce609fd..1a25337512 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -68,7 +68,6 @@ type 'a definition_entry = { const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_universes : universes_entry; - const_entry_opaque : bool; const_entry_inline_code : bool } type section_def_entry = { @@ -91,6 +90,7 @@ type primitive_entry = { type 'a constant_entry = | DefinitionEntry of 'a definition_entry + | OpaqueEntry of 'a definition_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a980d22e42..c99edccda7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff = | OpaqueDef b -> b | Def b -> Mod_subst.force_constr b | _ -> assert false in + if Declareops.is_opaque cb then + OpaqueEntry { + const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some cb.const_type; + const_entry_universes = univs; + const_entry_inline_code = cb.const_inline_code } + else DefinitionEntry { const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } let export_eff eff = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 165feca1b6..e28849c953 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,9 +115,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; + | OpaqueEntry ({ const_entry_type = typ; const_entry_universes = Monomorphic_entry univs; _ } as c) -> + let typ = match typ with None -> assert false | Some typ -> typ in let env = push_context_set ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in @@ -155,12 +155,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } - (** Similar case for polymorphic entries. TODO: also delay type-checking of - the body. *) + (** Similar case for polymorphic entries. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; + | OpaqueEntry ({ const_entry_type = typ; const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let typ = match typ with None -> assert false | Some typ -> typ in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in @@ -200,7 +199,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in (* Opaque constants must be provided with a non-empty const_entry_type, and thus should have been treated above. *) - let () = assert (not c.const_entry_opaque) in let body, ctx = match trust with | Pure -> let (body, ctx), () = Future.join body in @@ -375,7 +373,6 @@ let translate_local_def env _id centry = const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; - const_entry_opaque = false; const_entry_inline_code = false; } in let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in |