diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-06 18:02:25 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-11 11:17:10 +0200 |
| commit | b247761476c4b36f0945c19c23c171ea57701178 (patch) | |
| tree | 95733168d350fd3c014c1eb7f7792c6bc3d431f4 /kernel/safe_typing.ml | |
| parent | 009718d9d0130a967261ae5d2484985522fc2f7c (diff) | |
Fix for bug #4863, update the Proofview's env with
side_effects. Partial solution to the handling of side effects
in proofview.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 7 |
1 files changed, 0 insertions, 7 deletions
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; |