diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:43:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:17:20 +0200 |
| commit | f34dcb97406611704c93970ea623d6a8587e5ba8 (patch) | |
| tree | 5a636c498c4c3fad7c15cc266dd8a386b85123e1 /plugins | |
| parent | e5b355107d985d7efe2976b9eee9b6c182e25f24 (diff) | |
Moving the remaining Refiner functions to Tacmach.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e7c75e029e..878f7a834e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -201,7 +201,7 @@ let exec_tactic env evd n f args = (* Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in - let evd = Evd.minimize_universes (Refiner.project gls) in + let evd = Evd.minimize_universes gls.Evd.sigma in let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5c25db1a82..5f463f8de4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0 (* }}} *) let pf_merge_uc uc gl = - re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc) + re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc) let pf_merge_uc_of sigma gl = let ucst = Evd.evar_universe_context sigma in pf_merge_uc ucst gl |