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

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

6 files changed, 16 insertions, 11 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/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6ed61043f9..767a9ec39b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
       let constructors = Inductiveops.get_constructors env indf in
       let constructor : Inductiveops.constructor_summary =
         List.find
-          (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr))
+          (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr))
           (Array.to_list constructors)
       in
       let cs_args_types : types list =
@@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ =
       let constructors = Inductiveops.get_constructors env indf in
       let constructor =
         List.find
-          (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr)
+          (fun cs ->
+            Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr)
           (Array.to_list constructors)
       in
       let cs_args_types : types list =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8e1331ace9..164a446fe3 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -444,7 +444,8 @@ let rec are_unifiable_aux = function
     match (DAst.get l, DAst.get r) with
     | PatVar _, _ | _, PatVar _ -> are_unifiable_aux eqs
     | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) ->
-      if not (eq_constructor constructor2 constructor1) then raise NotUnifiable
+      if not (Construct.CanOrd.equal constructor2 constructor1) then
+        raise NotUnifiable
       else
         let eqs' =
           try List.combine cpl1 cpl2 @ eqs
@@ -464,7 +465,8 @@ let rec eq_cases_pattern_aux = function
     match (DAst.get l, DAst.get r) with
     | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
     | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) ->
-      if not (eq_constructor constructor2 constructor1) then raise NotUnifiable
+      if not (Construct.CanOrd.equal constructor2 constructor1) then
+        raise NotUnifiable
       else
         let eqs' =
           try List.combine cpl1 cpl2 @ eqs
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