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 /proofs/refine.ml | |
| parent | 3d162ca9095ff9299be5cc8847636a36b8e49f1e (diff) | |
Remove the side-effect role from the kernel.
We move the role data into the evarmap instead.
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 8439156e65..d0e89183a8 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -60,7 +60,7 @@ let generic_refine ~typecheck f gl = let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in - let env = Safe_typing.push_private_constants env privates_csts in + let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in |