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/ssr | |
| parent | e5b355107d985d7efe2976b9eee9b6c182e25f24 (diff) | |
Moving the remaining Refiner functions to Tacmach.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |