diff options
| author | Pierre-Marie Pédrot | 2019-05-22 17:46:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-26 01:14:38 +0200 |
| commit | 1e83ae578feea41d34c3ba26a1f74c3c715620a2 (patch) | |
| tree | c67f5fd826c315191bfa666cd5e025ff396534cc /kernel/safe_typing.ml | |
| parent | 51dc650f8b47a7381c19376793871817f2ef9578 (diff) | |
More precise type for Safe_typing export and inlining of private constants.
We get rid of the future wrappers, as all callers are immediately forcing
the result.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 26 |
1 files changed, 6 insertions, 20 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 873cc2a172..a90631c0f1 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -648,18 +648,10 @@ let inline_side_effects env body side_eff = let body = List.fold_right fold_arg args body in (body, ctx, sigs) -let inline_private_constants_in_definition_entry env ce = - let open Entries in - { ce with - const_entry_body = Future.chain - ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx',_ = inline_side_effects env body side_eff in - let ctx' = Univ.ContextSet.union ctx ctx' in - (body, ctx'), ()); - } - -let inline_private_constants_in_constr env body side_eff = - pi1 (inline_side_effects env body side_eff) +let inline_private_constants env ((body, ctx), side_eff) = + let body, ctx',_ = inline_side_effects env body side_eff in + let ctx' = Univ.ContextSet.union ctx ctx' in + (body, ctx') let is_suffix l suf = match l with | [] -> false @@ -712,13 +704,7 @@ let constant_entry_of_side_effect eff = let export_eff eff = (eff.seff_constant, eff.seff_body, eff.seff_role) -let export_side_effects mb env c = - let open Entries in - let body = c.const_entry_body in - let _, eff = Future.force body in - let ce = { c with - Entries.const_entry_body = Future.chain body - (fun (b_ctx, _) -> b_ctx, ()) } in +let export_side_effects mb env (b_ctx, eff) = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in @@ -742,7 +728,7 @@ let export_side_effects mb env c = in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, ce + | [] -> List.rev acc, b_ctx | eff :: rest -> if Int.equal sl 0 then let env, cb = |