Merge PR #13075: Introducing the foundations for a name-alias-agnostic API

Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index dc5fd80f9e..bdf3495479 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -91,7 +91,7 @@ let case_style_eq s1 s2 = let open Constr in match s1, s2 with
 let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
   | PatVar na1, PatVar na2 -> Name.equal na1 na2
   | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
-    eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+    Construct.CanOrd.equal c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
       Name.equal na1 na2
   | (PatVar _ | PatCstr _), _ -> false
 
@@ -109,7 +109,7 @@ let matching_var_kind_eq k1 k2 = match k1, k2 with
 
 let tomatch_tuple_eq f (c1, p1) (c2, p2) =
   let eqp {CAst.v=(i1, na1)} {CAst.v=(i2, na2)} =
-    eq_ind i1 i2 && List.equal Name.equal na1 na2
+    Ind.CanOrd.equal i1 i2 && List.equal Name.equal na1 na2
   in
   let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
   f c1 c2 && eq_pred p1 p2