From 2b91a8989687e152f7120aa6c907ffeba8495bab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 10:44:51 +0200
Subject: Deprecate the non-qualified equality functions on kerpairs.

This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
---
 tactics/cbn.ml     | 2 +-
 tactics/tactics.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 0b13f4763a..bec9ede6f1 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -225,7 +225,7 @@ 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
+        Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2
       | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
       | _, _ -> false
     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"
-- 
cgit v1.2.3


From 0590764209dcb8540b5292aca38fe2df38b90ab9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 14:19:20 +0200
Subject: Same little game with Projection.

---
 tactics/cbn.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index bec9ede6f1..5838bbcc19 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -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
-- 
cgit v1.2.3


From 0a46af10ffc38726207bca952775102d48ad3b15 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 18:36:10 +0200
Subject: Rename the GlobRef comparison modules following the standard pattern.

---
 tactics/btermdn.ml   | 2 +-
 tactics/term_dnet.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

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/term_dnet.ml b/tactics/term_dnet.ml
index 3bcd235b41..fee9dd1b96 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -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)
-- 
cgit v1.2.3


From bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 12:42:21 +0200
Subject: Introduce an Ind module in the Names API.

This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
---
 tactics/elim.ml      | 2 +-
 tactics/term_dnet.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

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/term_dnet.ml b/tactics/term_dnet.ml
index fee9dd1b96..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
-- 
cgit v1.2.3


From aa3d78fefde6897a50273c83f944b6617963a9bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 13:58:13 +0200
Subject: Similar introduction of a Construct module in the Names API.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3


From 9a3d4e284a03942e8a2b1f9d87a0b349702eaaa9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 17:56:33 +0200
Subject: Add missing deprecations in Projection API.

---
 tactics/cbn.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 5838bbcc19..31873ea6b0 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -226,7 +226,7 @@ struct
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
         Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2
-      | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
+      | Cst_proj p1, Cst_proj p2 -> Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2)
       | _, _ -> false
     in
     let rec equal_rec sk1 sk2 =
-- 
cgit v1.2.3