diff options
| author | Gaëtan Gilbert | 2020-01-30 23:34:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-30 23:34:49 +0100 |
| commit | a7af2f6571d007b6f83a1ec9252b52f69907a965 (patch) | |
| tree | 014747da5aa139b93c3c6d3e015499bbfb525541 /kernel | |
| parent | 92a294ca53752b61b0270a719826ffc759a25e8d (diff) | |
export_private_constants doesn't use the [constr in_univ_ctx] argument
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 10 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f6f2058c13..2047fd5fc5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -757,7 +757,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 +774,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 +803,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 +817,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 diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 92bbd264fa..c879481c66 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -84,8 +84,8 @@ type side_effect_declaration = type exported_private_constant = Constant.t val export_private_constants : - private_constants Entries.proof_output -> - (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer + private_constants -> + exported_private_constant list safe_transformer (** returns the main constant *) val add_constant : |