aboutsummaryrefslogtreecommitdiff
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 38b26d06b9..a7ebd5f9f5 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
let same_proj sigma t1 t2 =
match EConstr.kind sigma t1, EConstr.kind sigma t2 with
- | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2
+ | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2
| _ -> false
let all_ok _ _ = true