aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-23 17:56:33 +0200
committerPierre-Marie Pédrot2020-10-21 12:27:39 +0200
commit9a3d4e284a03942e8a2b1f9d87a0b349702eaaa9 (patch)
tree796075d0664347a8704fd53ca1a96a0d1a48abfd /plugins
parent373376b734343d86aecc8d1f91a8c78eefa2b6cc (diff)
Add missing deprecations in Projection API.
Diffstat (limited to 'plugins')
-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