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.

10 files changed, 18 insertions, 18 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a459229256..d48951e84a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -514,7 +514,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
@@ -1936,7 +1936,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.");
@@ -2164,7 +2164,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 71ef166ff0..0200b32ef2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -245,7 +245,7 @@ let matches_core env sigma allow_bound_rels
     match ref, EConstr.kind sigma c with
     | VarRef id, Var id' -> Names.Id.equal id id'
     | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
-    | IndRef i, Ind (i', _) -> Names.eq_ind i i'
+    | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
     | _, _ -> false
   in
@@ -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 08cb173442..baab41fa26 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -570,7 +570,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         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
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index dc5fd80f9e..43032790e2 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -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/patternops.ml b/pretyping/patternops.ml
index 8c3d624f0f..b5c83b75f9 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
 
@@ -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 d94cae75bd..9cf7119709 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -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 08303c80d6..4d37c0ef60 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -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'