aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrequality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
-rw-r--r--plugins/ssr/ssrequality.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 859513d5c..57635edac 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