diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ee101400d6..8db8a044a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -321,6 +321,8 @@ let universes_of_private eff = let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env +let structure_body_of_safe_env env = env.revstruct + let sections_of_safe_env senv = senv.sections let get_section = function @@ -757,7 +759,7 @@ let translate_direct_opaque env kn ce = let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } -let export_side_effects mb env (b_ctx, eff) = +let export_side_effects mb env eff = let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl @@ -774,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) = in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, b_ctx + | [] -> List.rev acc | eff :: rest -> if Int.equal sl 0 then let env, cb = @@ -803,8 +805,8 @@ let push_opaque_proof pf senv = let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in senv, o -let export_private_constants ce senv = - let exported, ce = export_side_effects senv.revstruct senv.env ce in +let export_private_constants eff senv = + let exported = export_side_effects senv.revstruct senv.env eff in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> let local = empty_private c.const_universes in @@ -817,7 +819,7 @@ let export_private_constants ce senv = let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) let senv = List.fold_left add_constant_aux senv bodies in - (ce, exported), senv + exported, senv let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in @@ -908,14 +910,19 @@ let check_mind mie lab = (* The label and the first inductive type name should match *) assert (Id.equal (Label.to_id lab) oie.mind_entry_typename) +let add_checked_mind kn mib senv = + let mib = + match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + in + add_field (MutInd.label kn,SFBmind mib) (I kn) senv + let add_mind l mie senv = let () = check_mind mie l in let kn = MutInd.make2 senv.modpath l in - let mib = Indtypes.check_inductive senv.env kn mie in - let mib = - match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + let sec_univs = Option.map Section.all_poly_univs senv.sections in - kn, add_field (l,SFBmind mib) (I kn) senv + let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in + kn, add_checked_mind kn mib senv (** Insertion of module types *) @@ -1014,9 +1021,8 @@ let close_section senv = add_constant_aux senv (kn, cb) | `Inductive (ind, mib) -> let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in - let mie = Cooking.cook_inductive info mib in - let _, senv = add_mind (MutInd.label ind) mie senv in - senv + let mib = Cooking.cook_inductive info mib in + add_checked_mind ind mib senv in List.fold_left fold senv redo |