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 | |
| parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) | |
Deprecate UState aliases in Evd.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 |
2 files changed, 2 insertions, 2 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 diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 00c971237..7f0b77c9e 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -216,7 +216,7 @@ let same_proj sigma t1 t2 = let all_ok _ _ = true let fake_pmatcher_end () = - mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp) + mkProp, L2R, (Evd.empty, UState.empty, mkProp) let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in |