diff options
| -rw-r--r-- | kernel/entries.ml | 11 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 12 | ||||
| -rw-r--r-- | tactics/declare.ml | 13 |
4 files changed, 21 insertions, 17 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index ca08ba485e..bc389e9fcf 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -57,17 +57,15 @@ type mutual_inductive_entry = { } (** {6 Constants (Definition/Axiom) } *) -type 'a proof_output = constr Univ.in_universe_context_set * 'a -type 'a const_entry_body = 'a proof_output Future.computation type definition_entry = { - const_entry_body : constr Univ.in_universe_context_set; + const_entry_body : constr; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; - const_entry_type : types option; - const_entry_universes : universes_entry; + const_entry_type : types option; + const_entry_universes : universes_entry; const_entry_inline_code : bool } type section_def_entry = { @@ -98,6 +96,9 @@ type primitive_entry = { prim_entry_content : CPrimitives.op_or_type; } +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation + type 'a constant_entry = | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7526508c4e..2c434d4edf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff = } else DefinitionEntry { - const_entry_body = (p, Univ.ContextSet.empty); + const_entry_body = p; const_entry_secctx = Some cb.const_hyps; const_entry_feedback = None; const_entry_type = Some cb.const_type; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b3c3dcbf45..5844bd89f8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -194,14 +194,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in - let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let () = match trust with | Pure -> () | SideEffects _ -> assert false in let env, usubst, univs = match c.const_entry_universes with - | Monomorphic_entry univs -> - let ctx = Univ.ContextSet.union univs ctx in + | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> @@ -210,10 +209,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - let () = - if not (Univ.ContextSet.is_empty ctx) then - CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") - in env, sbst, Polymorphic auctx in let j = Typeops.infer env body in @@ -347,9 +342,8 @@ let translate_recipe env _kn r = let translate_local_def env _id centry = let open Cooking in - let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { - const_entry_body = body; + const_entry_body = centry.secdef_body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; diff --git a/tactics/declare.ml b/tactics/declare.ml index 74196bb875..aa94ab5a25 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -173,12 +173,21 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types let cast_proof_entry e = let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in + let univs = + if Univ.ContextSet.is_empty ctx then e.proof_entry_universes + else match e.proof_entry_universes with + | Monomorphic_entry ctx' -> + (* This can actually happen, try compiling EqdepFacts for instance *) + Monomorphic_entry (Univ.ContextSet.union ctx' ctx) + | Polymorphic_entry _ -> + anomaly Pp.(str "Local universes in non-opaque polymorphic definition."); + in { - const_entry_body = (body, ctx); + const_entry_body = body; const_entry_secctx = e.proof_entry_secctx; const_entry_feedback = e.proof_entry_feedback; const_entry_type = e.proof_entry_type; - const_entry_universes = e.proof_entry_universes; + const_entry_universes = univs; const_entry_inline_code = e.proof_entry_inline_code; } |