aboutsummaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
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 /pretyping/patternops.ml
parent373376b734343d86aecc8d1f91a8c78eefa2b6cc (diff)
Add missing deprecations in Projection API.
Diffstat (limited to 'pretyping/patternops.ml')
-rw-r--r--pretyping/patternops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b5c83b75f9..b259945d9e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -59,7 +59,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PCoFix (i1,f1), PCoFix (i2,f2) ->
Int.equal i1 i2 && rec_declaration_eq f1 f2
| PProj (p1, t1), PProj (p2, t2) ->
- Projection.equal p1 p2 && constr_pattern_eq t1 t2
+ Projection.CanOrd.equal p1 p2 && constr_pattern_eq t1 t2
| PInt i1, PInt i2 ->
Uint63.equal i1 i2
| PFloat f1, PFloat f2 ->