diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-02 14:58:00 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-06 13:41:24 +0100 |
commit | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (patch) | |
tree | 06dc436ba2d41764b5bbe48c311bdaeaf5c1514c /plugins/ssr/ssrcommon.ml | |
parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) |
Deprecate UState aliases in Evd.
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
-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 5163ec7b3..e2ec8d72a 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1193,7 +1193,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl else if to_ind && occ = None then let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in - let ucst = Evd.union_evar_universe_context ucst ucst' in + let ucst = UState.union ucst ucst' in if nv = 0 then anomaly "occur_existential but no evars" else let gl, pty = pfe_type_of gl p in false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl |