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

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

6 files changed, 9 insertions, 9 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index f721e9956b..af0ca22868 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -27,7 +27,7 @@ type term_label =
 | SortLabel
 
 let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
+| GRLabel gr1, GRLabel gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | _ -> pervasives_compare t1 t2 (** OK *)
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 0b13f4763a..31873ea6b0 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -225,8 +225,8 @@ struct
     let equal_cst_member x y =
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
-        Constant.equal c1 c2 && Univ.Instance.equal u1 u2
-      | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
+        Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2
+      | Cst_proj p1, Cst_proj p2 -> Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2)
       | _, _ -> false
     in
     let rec equal_rec sk1 sk2 =
@@ -239,7 +239,7 @@ struct
       | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 ->
         f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
       | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
-        Projection.Repr.equal (Projection.repr p) (Projection.repr p2)
+        Projection.Repr.CanOrd.equal (Projection.repr p) (Projection.repr p2)
         && equal_rec s1 s2
       | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
         f_fix f1 f2
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 49437a2aef..9a55cabc86 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -193,7 +193,7 @@ let head_in indl t gl =
   let sigma = Tacmach.New.project gl in
   try
     let ity,_ = extract_mrectype sigma t in
-    List.exists (fun i -> eq_ind (fst i) (fst ity)) indl
+    List.exists (fun i -> Ind.CanOrd.equal (fst i) (fst ity)) indl
   with Not_found -> false
 
 let decompose_these c l =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 60e2db4dce..486575d229 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -768,7 +768,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
           in
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
-          if eq_constructor sp1 sp2 then
+          if Construct.CanOrd.equal sp1 sp2 then
             let nparams = inductive_nparams env ind1 in
             let params1,rargs1 = List.chop nparams args1 in
             let _,rargs2 = List.chop nparams args2 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a607c09010..f3ecc2a9f0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -540,7 +540,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   | (f, n, ar) :: oth ->
     let open Context.Named.Declaration in
     let (sp', u')  = check_mutind env sigma n ar in
-    if not (MutInd.equal sp sp') then
+    if not (QMutInd.equal env sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 3bcd235b41..df07dcbca7 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -91,7 +91,7 @@ struct
     | DArray (t,def,ty) -> DArray(Array.map f t, f def, f ty)
 
   let compare_ci ci1 ci2 =
-    let c = ind_ord ci1.ci_ind ci2.ci_ind in
+    let c = Ind.CanOrd.compare ci1.ci_ind ci2.ci_ind in
     if c = 0 then
       let c = Int.compare ci1.ci_npar ci2.ci_npar in
       if c = 0 then
@@ -107,7 +107,7 @@ struct
   | DRel, _ -> -1 | _, DRel -> 1
   | DSort, DSort -> 0
   | DSort, _ -> -1 | _, DSort -> 1
-  | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2
+  | DRef gr1, DRef gr2 -> GlobRef.CanOrd.compare gr1 gr2
   | DRef _, _ -> -1 | _, DRef _ -> 1
 
   | DCtx (tl1, tr1), DCtx (tl2, tr2)