diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-18 18:16:43 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:12:28 +0200 |
commit | 665256fec8465ff0adb943063c25f07a6ca54618 (patch) | |
tree | dd0b48cf99153e80a655c4e708692e9c4b2a8feb /vernac | |
parent | ce830b204ad52f8b3655d2cb4672662120d83101 (diff) |
Statically ensuring that inlined entries out of the kernel have no effects.
This was an easy to prove property that I somehow overlooked.
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/obligations.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 02067c190..28aeaa725 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx = id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, eff = Future.force entry.const_entry_body in - assert(Safe_typing.empty_private_constants = eff); + let body, () = Future.force entry.const_entry_body in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' @@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf = let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in - let (body, cstr), eff = Future.force entry.Entries.const_entry_body in - assert(Safe_typing.empty_private_constants = eff); + let (body, cstr), () = Future.force entry.Entries.const_entry_body in let sigma = Evd.from_ctx (fst uctx) in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) body; |