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.

4 files changed, 9 insertions, 7 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e50c6087bb..73eb943418 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
            |Prod _ ->
             let new_infos = {dyn_infos with info = (f, args)} in
             build_proof_args env sigma do_finalize new_infos
-          | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
+          | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) ->
             let new_infos = {dyn_infos with info = (f, args)} in
             (*                    Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
             build_proof_args env sigma do_finalize new_infos
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1ab747ca09..0ab9ac65d7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match Constr.kind c with
-    | Ind ((u, _), _) -> MutInd.equal u rel_as_kn
-    | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn
+    | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn
+    | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn
     | _ -> false
   in
   let get_fun_num c =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 012fcee486..314c8abcaf 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
   let prop_sort = Sorts.InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+    let eq c1 c2 = Environ.QConstant.equal env c1 c2 in
     List.map
-      (function
-        | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
+      (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes)
       funs
   in
   let ind_list =
@@ -2228,7 +2228,8 @@ let build_case_scheme fa =
   let prop_sort = Sorts.InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal funs this_block_funs_indexes
+    let eq c1 c2 = Environ.QConstant.equal env c1 c2 in
+    List.assoc_f eq funs this_block_funs_indexes
   in
   let ind, sf =
     let ind = (first_fun_kn, funs_indexes) in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5d631aac84..118a917381 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -27,12 +27,13 @@ open Indfun_common
 *)
 let revert_graph kn post_tac hid =
   Proofview.Goal.enter (fun gl ->
+      let env = Proofview.Goal.env gl in
       let sigma = project gl in
       let typ = pf_get_hyp_typ hid gl in
       match EConstr.kind sigma typ with
       | App (i, args) when isInd sigma i ->
         let ((kn', num) as ind'), u = destInd sigma i in
-        if MutInd.equal kn kn' then
+        if Environ.QMutInd.equal env kn kn' then
           (* We have generated a graph hypothesis so that we must change it if we can *)
           let info =
             match find_Function_of_graph ind' with