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

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

13 files changed, 45 insertions, 45 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 97218ca670..4a29db0dcf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -515,7 +515,7 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
       let loc = pat.CAst.loc in
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
-      if eq_ind ind' ind then
+      if Ind.CanOrd.equal ind' ind then
         (* Check the constructor has the right number of args *)
         let ci = cstrs.(i-1) in
         let nb_args_constr = ci.cs_nargs in
@@ -1965,7 +1965,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
           let realnal =
             match t with
               | Some {CAst.loc;v=(ind',realnal)} ->
-                  if not (eq_ind ind ind') then
+                  if not (Ind.CanOrd.equal ind ind') then
                     user_err ?loc  (str "Wrong inductive type.");
                   if not (Int.equal nrealargs_ctxt (List.length realnal)) then
                       anomaly (Pp.str "Ill-formed 'in' clause in cases.");
@@ -2193,7 +2193,7 @@ let constr_of_pat env sigma arsign pat avoid =
         in
         let (ind,u), params = dest_ind_family indf in
         let params = List.map EConstr.of_constr params in
-        if not (eq_ind ind cind) then error_bad_constructor ?loc env cstr ind;
+        if not (Ind.CanOrd.equal ind cind) then error_bad_constructor ?loc env cstr ind;
         let cstrs = get_constructors env indf in
         let ci = cstrs.(i-1) in
         let nb_args_constr = ci.cs_nargs in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d759f82d35..6e6189796e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -119,7 +119,7 @@ let disc_subset sigma x =
        Ind (i,_) ->
          let len = Array.length l in
          let sigty = delayed_force sig_typ in
-           if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty)
+           if Int.equal len 2 && Ind.CanOrd.equal i (Globnames.destIndRef sigty)
            then
              let (a, b) = pair_of_array l in
                Some (a, b)
@@ -240,10 +240,10 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
          let sigT = delayed_force sigT_typ in
          let prod = delayed_force prod_typ in
          (* Sigma types *)
-         if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
-            && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod))
+         if Int.equal len (Array.length l') && Int.equal len 2 && Ind.CanOrd.equal i i'
+            && (Ind.CanOrd.equal i (destIndRef sigT) || Ind.CanOrd.equal i (destIndRef prod))
          then
-           if eq_ind i (destIndRef sigT)
+           if Ind.CanOrd.equal i (destIndRef sigT)
            then
              begin
                let (a, pb), (a', pb') =
@@ -303,7 +303,7 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
                      papp sigma prod_intro [| a'; b'; x ; y |])
              end
          else
-         if eq_ind i i' && Int.equal len (Array.length l') then
+         if Ind.CanOrd.equal i i' && Int.equal len (Array.length l') then
            (try subco sigma
             with NoSubtacCoercion ->
               let sigma, typ = Typing.type_of env sigma c in
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 0c3eaa1da9..8ddc576d83 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -57,7 +57,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
   | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
   | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
-  | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
+  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
   | _ -> pervasives_compare t1 t2 (** OK *)
 
 module ClTyp = struct
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 419eeaa92a..a3f1c0b004 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -244,9 +244,9 @@ let matches_core env sigma allow_bound_rels
     let open GlobRef in
     match ref, EConstr.kind sigma c with
     | VarRef id, Var id' -> Names.Id.equal id id'
-    | ConstRef c, Const (c',_) -> Constant.equal c c'
-    | IndRef i, Ind (i', _) -> Names.eq_ind i i'
-    | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
+    | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
+    | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i'
+    | ConstructRef c, Construct (c',u) -> Names.Construct.CanOrd.equal c c'
     | _, _ -> false
   in
   let rec sorec ctx env subst p t =
@@ -307,11 +307,11 @@ let matches_core env sigma allow_bound_rels
 
       | PApp (c1,arg1), App (c2,arg2) ->
         (match c1, EConstr.kind sigma c2 with
-        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
+        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Environ.QConstant.equal env r (Projection.constant pr))
             || Projection.unfolded pr ->
           raise PatternMatchingFailure
         | PProj (pr1,c1), Proj (pr,c) ->
-          if Projection.equal pr1 pr then
+          if Environ.QProjection.equal env pr1 pr then
             try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
             with Invalid_argument _ -> raise PatternMatchingFailure
           else raise PatternMatchingFailure
@@ -324,7 +324,7 @@ let matches_core env sigma allow_bound_rels
           with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
-        when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) ->
+        when Projection.unfolded pr || not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
         raise PatternMatchingFailure
 
       | PApp (c, args), Proj (pr, c2) ->
@@ -332,7 +332,7 @@ let matches_core env sigma allow_bound_rels
                sorec ctx env subst p term
          with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 
-      | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
+      | PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 ->
           sorec ctx env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
@@ -374,7 +374,7 @@ let matches_core env sigma allow_bound_rels
           | Some ind1 ->
             (* ppedrot: Something spooky going here. The comparison used to be
                the generic one, so I may have broken something. *)
-            if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure
+            if not (Ind.CanOrd.equal ind1 ci2.ci_ind) then raise PatternMatchingFailure
           in
           let () =
             if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a5311e162d..90af143a2d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -387,7 +387,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
     | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
-       if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+       if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
@@ -429,7 +429,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
           (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
     | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
-       if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+       if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
@@ -566,11 +566,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     in
     let compare_heads evd =
       match EConstr.kind evd term, EConstr.kind evd term' with
-      | Const (c, u), Const (c', u') when Constant.equal c c' ->
+      | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
         let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
         check_strict evd u u'
       | Const _, Const _ -> UnifFailure (evd, NotSameHead)
-      | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' ->
+      | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
         if EInstance.is_empty u && EInstance.is_empty u' then Success evd
         else
           let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
@@ -589,7 +589,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           end
       | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
       | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
-        when Names.eq_constructor cons cons' ->
+        when Names.Construct.CanOrd.equal cons cons' ->
         if EInstance.is_empty u && EInstance.is_empty u' then Success evd
         else
           let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
@@ -831,7 +831,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         in
         ise_try evd [f1; f2]
 
-        | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' ->
+        | Proj (p, c), Proj (p', c') when QProjection.Repr.equal env (Projection.repr p) (Projection.repr p') ->
           let f1 i =
             ise_and i
             [(fun i -> evar_conv_x flags env i CONV c c');
@@ -844,7 +844,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
             ise_try evd [f1; f2]
 
         (* Catch the p.c ~= p c' cases *)
-        | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' ->
+        | Proj (p,c), Const (p',u) when QConstant.equal env (Projection.constant p) p' ->
           let res =
             try Some (destApp evd (Retyping.expand_projection env evd p c []))
             with Retyping.RetypeError _ -> None
@@ -855,7 +855,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                 appr2
             | None -> UnifFailure (evd,NotSameHead))
 
-        | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
+        | Const (p,u), Proj (p',c') when QConstant.equal env p (Projection.constant p') ->
           let res =
             try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
             with Retyping.RetypeError _ -> None
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index eaf8c65811..13abf47413 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -206,7 +206,7 @@ let is_array_const env sigma c =
   | Const (cst,_) ->
     (match env.Environ.retroknowledge.Retroknowledge.retro_array with
      | None -> false
-     | Some cst' -> Constant.equal cst cst')
+     | Some cst' -> Environ.QConstant.equal env cst cst')
   | _ -> false
 
 let split_as_array env sigma0 = function
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index dc5fd80f9e..bdf3495479 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -91,7 +91,7 @@ let case_style_eq s1 s2 = let open Constr in match s1, s2 with
 let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
   | PatVar na1, PatVar na2 -> Name.equal na1 na2
   | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
-    eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+    Construct.CanOrd.equal c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
       Name.equal na1 na2
   | (PatVar _ | PatCstr _), _ -> false
 
@@ -109,7 +109,7 @@ let matching_var_kind_eq k1 k2 = match k1, k2 with
 
 let tomatch_tuple_eq f (c1, p1) (c2, p2) =
   let eqp {CAst.v=(i1, na1)} {CAst.v=(i2, na2)} =
-    eq_ind i1 i2 && List.equal Name.equal na1 na2
+    Ind.CanOrd.equal i1 i2 && List.equal Name.equal na1 na2
   in
   let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
   f c1 c2 && eq_pred p1 p2
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5be8f9f83c..5ffd919312 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -584,7 +584,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
         (List.map
            (function ((mind',u'),dep',s') ->
               let (sp',_) = mind' in
-              if MutInd.equal sp sp' then
+              if QMutInd.equal env sp sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
                 ((mind',u'),mibi',mipi',dep',s')
               else
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
index 7a7099c195..dd3488c1df 100644
--- a/pretyping/keys.ml
+++ b/pretyping/keys.ml
@@ -34,7 +34,7 @@ module KeyOrdered = struct
 
   let hash gr =
     match gr with
-    | KGlob gr -> 9 + GlobRef.Ordered.hash gr
+    | KGlob gr -> 9 + GlobRef.CanOrd.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -49,14 +49,14 @@ module KeyOrdered = struct
 
   let compare gr1 gr2 =
     match gr1, gr2 with
-    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.compare gr1 gr2
     | _, KGlob _ -> -1
     | KGlob _, _ -> 1
     | k, k' -> Int.compare (hash k) (hash k')
 
   let equal k1 k2 =
     match k1, k2 with
-    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.equal gr1 gr2
     | _, KGlob _ -> false
     | KGlob _, _ -> false
     | k, k' -> k == k'
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8c3d624f0f..b259945d9e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -23,7 +23,7 @@ open Environ
 
 let case_info_pattern_eq i1 i2 =
   i1.cip_style == i2.cip_style &&
-  Option.equal eq_ind i1.cip_ind i2.cip_ind &&
+  Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind &&
   Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags &&
   i1.cip_extensible == i2.cip_extensible
 
@@ -59,7 +59,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PCoFix (i1,f1), PCoFix (i2,f2) ->
   Int.equal i1 i2 && rec_declaration_eq f1 f2
 | PProj (p1, t1), PProj (p2, t2) ->
-   Projection.equal p1 p2 && constr_pattern_eq t1 t2
+   Projection.CanOrd.equal p1 p2 && constr_pattern_eq t1 t2
 | PInt i1, PInt i2 ->
    Uint63.equal i1 i2
 | PFloat f1, PFloat f2 ->
@@ -547,7 +547,7 @@ and pats_of_glob_branches loc metas vars ind brs =
         true, [] (* ends with _ => _ *)
       | PatCstr((indsp,j),lv,_), _, _ ->
         let () = match ind with
-        | Some sp when eq_ind sp indsp -> ()
+        | Some sp when Ind.CanOrd.equal sp indsp -> ()
         | _ ->
           err ?loc (Pp.str "All constructors must be in the same inductive type.")
         in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 268ad2ae56..06f7d92e62 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -813,7 +813,7 @@ struct
             try
               let IndType (indf, args) = find_rectype !!env sigma ty in
               let ((ind',u'),pars) = dest_ind_family indf in
-              if eq_ind ind ind' then List.map EConstr.of_constr pars
+              if Ind.CanOrd.equal ind ind' then List.map EConstr.of_constr pars
               else (* Let the usual code throw an error *) []
             with Not_found -> []
       else []
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9d15e98373..9cf7119709 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -82,7 +82,7 @@ type evaluable_reference =
   | EvalEvar of EConstr.existential
 
 let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
-| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2
+| EvalConst c1, EvalConst c2 -> Constant.CanOrd.equal c1 c2
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
@@ -995,7 +995,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       | CoFix _ | Fix _ -> s'
       | Proj (p,t) when
           (match EConstr.kind sigma constr with
-          | Const (c', _) -> Constant.equal (Projection.constant p) c'
+          | Const (c', _) -> Constant.CanOrd.equal (Projection.constant p) c'
           | _ -> false) ->
         let npars = Projection.npars p in
           if List.length stack <= npars then
@@ -1101,7 +1101,7 @@ let contextually byhead occs f env sigma t =
 
 let match_constr_evaluable_ref sigma c evref =
   match EConstr.kind sigma c, evref with
-  | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u
+  | Const (c,u), EvalConstRef c' when Constant.CanOrd.equal c c' -> Some u
   | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
@@ -1324,7 +1324,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   if isIndRef ref then
     let ((mind,u),t) = reduce_to_ind_gen allow_product env sigma t in
     begin match ref with
-    | GlobRef.IndRef mind' when eq_ind mind mind' -> t
+    | GlobRef.IndRef mind' when Ind.CanOrd.equal mind mind' -> t
     | _ -> error_cannot_recognize ref
     end
   else
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ccfb508964..4d37c0ef60 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -547,10 +547,10 @@ let oracle_order env cf1 cf2 =
       | Some k2 ->
         match k1, k2 with
         | IsProj (p, _), IsKey (ConstKey (p',_))
-          when Constant.equal (Projection.constant p) p' ->
+          when Environ.QConstant.equal env (Projection.constant p) p' ->
           Some (not (Projection.unfolded p))
         | IsKey (ConstKey (p,_)), IsProj (p', _)
-          when Constant.equal p (Projection.constant p') ->
+          when Environ.QConstant.equal env p (Projection.constant p') ->
           Some (Projection.unfolded p')
         | _ ->
           Some (Conv_oracle.oracle_order (fun x -> x)
@@ -796,7 +796,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
         | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
 
         (* Fast path for projections. *)
-        | Proj (p1,c1), Proj (p2,c2) when Constant.equal
+        | Proj (p1,c1), Proj (p2,c2) when Environ.QConstant.equal env
             (Projection.constant p1) (Projection.constant p2) ->
           (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
                substn c1 c2
@@ -844,7 +844,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 
         | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
             (try
-             if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
+             if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
              let opt' = {opt with at_top = true; with_types = false} in
                Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true})
                (unirec_rec curenvnb CONV opt'
@@ -914,7 +914,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
         match EConstr.kind sigma c' with
         | Meta _ -> true
         | Evar _ -> true
-        | Const (c, u) -> Constant.equal c (Projection.constant p)
+        | Const (c, u) -> Environ.QConstant.equal env c (Projection.constant p)
         | _ -> false
       in
       let expand_proj c c' l =