From b247761476c4b36f0945c19c23c171ea57701178 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 18:02:25 +0200 Subject: Fix for bug #4863, update the Proofview's env with side_effects. Partial solution to the handling of side effects in proofview. --- kernel/safe_typing.ml | 7 ------- 1 file changed, 7 deletions(-) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 927278965..8b28cd87b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) -let constant_entry_of_private_constant = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.map (fun (_,kn,cb,eff_env) -> - kn, Term_typing.constant_entry_of_side_effect cb eff_env) l - let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in { Entries.from_env = CEphemeron.create env.revstruct; -- cgit v1.2.3