diff options
| author | Pierre-Marie Pédrot | 2019-05-13 00:03:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 20:19:37 +0200 |
| commit | e74fce3090323b4d3734f84ee8cf6dc1f5e85953 (patch) | |
| tree | 4c738543dd88e68759fe9c198f0c48d12e73c4e4 /proofs/refine.ml | |
| parent | 106a7c4a86e4c164a73cbc5a4c14f3c4ff527f30 (diff) | |
Abstract away the implementation of side-effects in Safe_typing.
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 06e6b89df1..4a9404aa96 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -44,17 +44,6 @@ let typecheck_evar ev env sigma = let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma -(* Get the side-effect's constant declarations to update the monad's - * environmnent *) -let add_if_undefined env eff = - let open Entries in - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env - -(* Add the side effects to the monad's environment, if not already done. *) -let add_side_effects env eff = - List.fold_left add_if_undefined env eff - let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -71,8 +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 sideff = Safe_typing.side_effects_of_private_constants privates_csts in - let env = add_side_effects env sideff in + let env = Safe_typing.push_private_constants env privates_csts 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 |