diff options
| author | Pierre-Marie Pédrot | 2020-02-04 17:53:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-04 17:53:34 +0100 |
| commit | b0116df798d4cef2ffaaf2ffbe8b60b06508436f (patch) | |
| tree | 208242a9c055195ce6f52a9a51460a85e28d9cfa /kernel/safe_typing.ml | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
| parent | c20fe3443f905dfea3ff746407cd1649ed8867ff (diff) | |
Merge PR #11491: Small side effect cleanup
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e8adde2605..8db8a044a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -759,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 @@ -776,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 = @@ -805,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 @@ -819,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 |