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, 7 insertions, 6 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 7a7e7d6e35..475d4e9af9 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -145,7 +145,7 @@ let build_beq_scheme_deps kn =
       | Cast (x,_,_) -> aux accu (Term.applist (x,a))
       | App _ -> assert false
       | Ind ((kn', _), _) ->
-          if MutInd.equal kn kn' then accu
+          if Environ.QMutInd.equal env kn kn' then accu
           else
             let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
             List.fold_left aux (eff :: accu) a
@@ -253,7 +253,7 @@ let build_beq_scheme mode kn =
         | Cast (x,_,_) -> aux (Term.applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
-            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+            if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
             else begin
               try
                 let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
@@ -539,7 +539,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp2,i2) ->
-  if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
+  Proofview.tclENV >>= fun env ->
+  if not (Environ.QMutInd.equal env sp1 sp2) || not (Int.equal i1 i2)
   then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5274a6da3b..7d0c5ee48f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -162,7 +162,7 @@ let cache_constant ((sp,kn), obj) =
     then Constant.make1 kn
     else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
   in
-  assert (Constant.equal kn' (Constant.make1 kn));
+  assert (Environ.QConstant.equal (Global.env ()) kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
   Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 356ccef06b..de72a30f18 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -405,7 +405,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
 let get_common_underlying_mutual_inductive env = function
   | [] -> assert false
   | (id,(mind,i as ind))::l as all ->
-      match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
+      match List.filter (fun (_,(mind',_)) -> not (Environ.QMutInd.equal env mind mind')) l with
       | (_,ind')::_ ->
           raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
       | [] ->
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 534c358a3f..79468627de 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -44,7 +44,7 @@ let find_mutually_recursive_statements sigma thms =
             [] in
       ind_hyps,ind_ccl) thms in
     let inds_hyps,ind_ccls = List.split inds in
-    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Names.MutInd.equal kn kn' in
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in
     (* Check if all conclusions are coinductive in the same type *)
     (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =