diff options
| author | Pierre-Marie Pédrot | 2019-06-05 10:35:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:07 +0200 |
| commit | e753855167e5629775b604128c6efc9d58ee626c (patch) | |
| tree | 7abdebb08679b76a80cf9d1a36f05b91a538c223 /vernac/comDefinition.ml | |
| parent | 3d162ca9095ff9299be5cc8847636a36b8e49f1e (diff) | |
Remove the side-effect role from the kernel.
We move the role data into the evarmap instead.
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 4cae4b8a74..1046e354a7 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -86,7 +86,7 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = if program_mode then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Safe_typing.empty_private_constants = sideff); + assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in |