diff options
37 files changed, 188 insertions, 125 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 28d23cc67e..1ac658f123 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -128,7 +128,7 @@ let isRefX sigma x c = let open GlobRef in match x, kind sigma c with | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' + | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' | VarRef id, Var id' -> Id.equal id id' | _ -> false diff --git a/engine/termops.ml b/engine/termops.ml index 3116b03c4f..031a505ce2 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1146,7 +1146,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 = | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 | Const (c, u), Const (c', u') -> Constant.CanOrd.equal c c' - | Ind (i, _), Ind (i', _) -> eq_ind i i' + | Ind (i, _), Ind (i', _) -> Ind.CanOrd.equal i i' | Construct (i, _), Construct (i', _) -> eq_constructor i i' | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 354809252e..4ca578affd 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -58,7 +58,7 @@ match t1, t2 with (eq_notation_constr vars) t1 t2 in let eqf (t1, (na1, o1)) (t2, (na2, o2)) = - let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in + let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 in Option.equal (eq_notation_constr vars) o1 o2 && @@ -1418,10 +1418,10 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 = let match_ind_pattern metas sigma ind pats a2 = match a2 with - | NRef (GlobRef.IndRef r2) when eq_ind ind r2 -> + | NRef (GlobRef.IndRef r2) when Ind.CanOrd.equal ind r2 -> sigma,(false,0,pats) | NApp (NRef (GlobRef.IndRef r2),l2) - when eq_ind ind r2 -> + when Ind.CanOrd.equal ind r2 -> let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats then diff --git a/kernel/constr.ml b/kernel/constr.ml index fb1e4d12da..b453a55d88 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -354,7 +354,7 @@ let isRefX x c = let open GlobRef in match x, kind c with | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' + | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' | VarRef id, Var id' -> Id.equal id id' | _ -> false @@ -955,7 +955,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2 | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2 | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) -> @@ -1139,7 +1139,7 @@ let constr_ord_int f t1 t2 = | App _, _ -> -1 | _, App _ -> 1 | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 - | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2 + | Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 @@ -1331,7 +1331,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Ind (ind,u) -> let u', hu = sh_instance u in (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) hu)) | Construct (c,u) -> let u', hu = sh_instance u in (Construct (sh_construct c, u'), @@ -1444,7 +1444,7 @@ let rec hash t = | Const (c,u) -> combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u)) | Ind (ind,u) -> - combinesmall 10 (combine (ind_hash ind) (Instance.hash u)) + combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u)) | Construct (c,u) -> combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) | Case (_ , p, iv, c, bl) -> @@ -1503,7 +1503,7 @@ struct let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in combine3 h1 h2 h3 let hash ci = - let h1 = ind_hash ci.ci_ind in + let h1 = Ind.CanOrd.hash ci.ci_ind in let h2 = Int.hash ci.ci_npar in let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index fdcf44c943..cb33bb729c 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -38,13 +38,13 @@ struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 + | IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2 | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 | _ -> false open Hashset.Combine let hash = function | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) - | IndRef i -> combinesmall 2 (ind_syntactic_hash i) + | IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i) | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) end diff --git a/kernel/declareops.ml b/kernel/declareops.ml index ee90ad382b..8de7123fee 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -157,7 +157,7 @@ let hcons_const_body cb = (** {6 Inductive types } *) let eq_nested_type t1 t2 = match t1, t2 with -| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2 +| NestedInd ind1, NestedInd ind2 -> Names.Ind.CanOrd.equal ind1 ind2 | NestedInd _, _ -> false | NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2 | NestedPrimitive _, _ -> false @@ -165,7 +165,7 @@ let eq_nested_type t1 t2 = match t1, t2 with let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true | Norec, _ -> false -| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 +| Mrec i1, Mrec i2 -> Names.Ind.CanOrd.equal i1 i2 | Mrec _, _ -> false | Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2 | Nested _, _ -> false diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2b1a295620..e34b3c0b47 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -404,7 +404,7 @@ let type_case_branches env (pind,largs) pj c = let check_case_info env (indsp,u) r ci = let (mib,mip as spec) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) || + not (Ind.CanOrd.equal indsp ci.ci_ind) || not (Int.equal mib.mind_nparams ci.ci_npar) || not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) || not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) || @@ -467,9 +467,9 @@ let inter_recarg r1 r2 = match r1, r2 with | Norec, _ -> None | Mrec i1, Mrec i2 | Nested (NestedInd i1), Nested (NestedInd i2) -| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None +| Mrec i1, (Nested (NestedInd i2)) -> if Names.Ind.CanOrd.equal i1 i2 then Some r1 else None | Mrec _, _ -> None -| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Nested (NestedInd i1), Mrec i2 -> if Names.Ind.CanOrd.equal i1 i2 then Some r2 else None | Nested (NestedInd _), _ -> None | Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) -> if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None @@ -556,7 +556,7 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | Mrec i | Nested (NestedInd i) -> eq_ind ind i + | Mrec i | Nested (NestedInd i) -> Ind.CanOrd.equal ind i | Norec | Nested (NestedPrimitive _) -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} @@ -667,7 +667,7 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' -> + | Nested (NestedInd kn') | Mrec kn' when Ind.CanOrd.equal (fst ind_kn) kn' -> build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end diff --git a/kernel/names.ml b/kernel/names.ml index f7658df355..b36a39ac79 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -600,18 +600,63 @@ module Mindmap = HMap.Make(MutInd.CanOrd) module Mindset = Mindmap.Set module Mindmap_env = HMap.Make(MutInd.UserOrd) +module Ind = +struct + (** Designation of a (particular) inductive type. *) + type t = MutInd.t (* the name of the inductive type *) + * int (* the position of this inductive type + within the block of mutually-recursive inductive types. + BEWARE: indexing starts from 0. *) + let modpath (mind, _) = MutInd.modpath mind + + module CanOrd = + struct + type nonrec t = t + let equal (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.CanOrd.equal m1 m2 + let compare (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c + let hash (m, i) = + Hashset.Combine.combine (MutInd.CanOrd.hash m) (Int.hash i) + end + + module UserOrd = + struct + type nonrec t = t + let equal (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 + let compare (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c + let hash (m, i) = + Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) + end + + module SyntacticOrd = + struct + type nonrec t = t + let equal (m1, i1) (m2, i2) = + Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 + + let compare (m1, i1) (m2, i2) = + let c = Int.compare i1 i2 in + if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c + + let hash (m, i) = + Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) + end + +end + (** Designation of a (particular) inductive type. *) -type inductive = MutInd.t (* the name of the inductive type *) - * int (* the position of this inductive type - within the block of mutually-recursive inductive types. - BEWARE: indexing starts from 0. *) +type inductive = Ind.t (** Designation of a (particular) constructor of a (particular) inductive type. *) type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) -let ind_modpath (mind,_) = MutInd.modpath mind +let ind_modpath = Ind.modpath let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) @@ -619,28 +664,17 @@ let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, _i) = ind let index_of_constructor (_ind, i) = i -let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 -let eq_user_ind (m1, i1) (m2, i2) = - Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2 -let eq_syntactic_ind (m1, i1) (m2, i2) = - Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2 - -let ind_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c -let ind_user_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c -let ind_syntactic_ord (m1, i1) (m2, i2) = - let c = Int.compare i1 i2 in - if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c - -let ind_hash (m, i) = - Hashset.Combine.combine (MutInd.hash m) (Int.hash i) -let ind_user_hash (m, i) = - Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) -let ind_syntactic_hash (m, i) = - Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i) +let eq_ind = Ind.CanOrd.equal +let eq_user_ind = Ind.UserOrd.equal +let eq_syntactic_ind = Ind.SyntacticOrd.equal + +let ind_ord = Ind.CanOrd.compare +let ind_user_ord = Ind.UserOrd.compare +let ind_syntactic_ord = Ind.SyntacticOrd.compare + +let ind_hash = Ind.CanOrd.hash +let ind_user_hash = Ind.UserOrd.hash +let ind_syntactic_hash = Ind.SyntacticOrd.hash let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let eq_user_constructor (ind1, j1) (ind2, j2) = @@ -665,20 +699,10 @@ let constructor_user_hash (ind, i) = let constructor_syntactic_hash (ind, i) = Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i) -module InductiveOrdered = struct - type t = inductive - let compare = ind_ord -end - -module InductiveOrdered_env = struct - type t = inductive - let compare = ind_user_ord -end - -module Indset = Set.Make(InductiveOrdered) -module Indset_env = Set.Make(InductiveOrdered_env) -module Indmap = Map.Make(InductiveOrdered) -module Indmap_env = Map.Make(InductiveOrdered_env) +module Indset = Set.Make(Ind.CanOrd) +module Indset_env = Set.Make(Ind.UserOrd) +module Indmap = Map.Make(Ind.CanOrd) +module Indmap_env = Map.Make(Ind.UserOrd) module ConstructorOrdered = struct type t = constructor diff --git a/kernel/names.mli b/kernel/names.mli index 76be6ca105..be53830af5 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -479,11 +479,39 @@ module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset module Mindmap_env : CMap.ExtS with type key = MutInd.t -(** Designation of a (particular) inductive type. *) -type inductive = MutInd.t (* the name of the inductive type *) - * int (* the position of this inductive type - within the block of mutually-recursive inductive types. - BEWARE: indexing starts from 0. *) +module Ind : +sig + (** Designation of a (particular) inductive type. *) + type t = MutInd.t (* the name of the inductive type *) + * int (* the position of this inductive type + within the block of mutually-recursive inductive types. + BEWARE: indexing starts from 0. *) + val modpath : t -> ModPath.t + + module CanOrd : sig + type nonrec t = t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + + module UserOrd : sig + type nonrec t = t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + + module SyntacticOrd : sig + type nonrec t = t + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + end + +end + +type inductive = Ind.t (** Designation of a (particular) constructor of a (particular) inductive type. *) type constructor = inductive (* designates the inductive type *) @@ -500,6 +528,8 @@ module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env val ind_modpath : inductive -> ModPath.t +[@@ocaml.deprecated "Use the Ind module"] + val constr_modpath : constructor -> ModPath.t val ith_mutual_inductive : inductive -> int -> inductive @@ -507,14 +537,23 @@ val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool +[@@ocaml.deprecated "Use the Ind module"] val eq_user_ind : inductive -> inductive -> bool +[@@ocaml.deprecated "Use the Ind module"] val eq_syntactic_ind : inductive -> inductive -> bool +[@@ocaml.deprecated "Use the Ind module"] val ind_ord : inductive -> inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_hash : inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_user_ord : inductive -> inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_user_hash : inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_syntactic_ord : inductive -> inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val ind_syntactic_hash : inductive -> int +[@@ocaml.deprecated "Use the Ind module"] val eq_constructor : constructor -> constructor -> bool val eq_user_constructor : constructor -> constructor -> bool val eq_syntactic_constructor : constructor -> constructor -> bool diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9314203e04..b5c4d6416a 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -65,11 +65,11 @@ type gname = let eq_gname gn1 gn2 = match gn1, gn2 with | Gind (s1, ind1), Gind (s2, ind2) -> - String.equal s1 s2 && eq_ind ind1 ind2 + String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.CanOrd.equal c1 c2 | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> - String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 + String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -96,7 +96,7 @@ open Hashset.Combine let gname_hash gn = match gn with | Gind (s, ind) -> - combinesmall 1 (combine (String.hash s) (ind_hash ind)) + combinesmall 1 (combine (String.hash s) (Ind.CanOrd.hash ind)) | Gconstant (s, c) -> combinesmall 2 (combine (String.hash s) (Constant.CanOrd.hash c)) | Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i)) @@ -107,7 +107,7 @@ let gname_hash gn = match gn with | Ginternal s -> combinesmall 8 (String.hash s) | Grel i -> combinesmall 9 (Int.hash i) | Gnamed id -> combinesmall 10 (Id.hash id) -| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i)) +| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (Ind.CanOrd.hash p) i)) let case_ctr = ref (-1) @@ -150,11 +150,11 @@ let eq_symbol sy1 sy2 = | SymbName n1, SymbName n2 -> Name.equal n1 n2 | SymbConst kn1, SymbConst kn2 -> Constant.CanOrd.equal kn1 kn2 | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2 - | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2 + | SymbInd ind1, SymbInd ind2 -> Ind.CanOrd.equal ind1 ind2 | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 - | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2 + | SymbProj (i1, k1), SymbProj (i2, k2) -> Ind.CanOrd.equal i1 i2 && Int.equal k1 k2 | _, _ -> false let hash_symbol symb = @@ -164,11 +164,11 @@ let hash_symbol symb = | SymbName name -> combinesmall 3 (Name.hash name) | SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c) | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw) - | SymbInd ind -> combinesmall 6 (ind_hash ind) + | SymbInd ind -> combinesmall 6 (Ind.CanOrd.hash ind) | SymbMeta m -> combinesmall 7 m | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) - | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k) + | SymbProj (i, k) -> combinesmall 10 (combine (Ind.CanOrd.hash i) k) module HashedTypeSymbol = struct type t = symbol @@ -438,7 +438,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) -> String.equal pf1 pf2 && - eq_ind ind1 ind2 && + Ind.CanOrd.equal ind1 ind2 && Int.equal tag1 tag2 && Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2 | MLint i1, MLint i2 -> @@ -457,7 +457,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) -> - String.equal s1 s2 && eq_ind ind1 ind2 && + String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 && eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | @@ -527,7 +527,7 @@ let rec hash_mllambda gn n env t = combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br) | MLconstruct (pf, ind, tag, args) -> let hpf = String.hash pf in - let hcs = ind_hash ind in + let hcs = Ind.CanOrd.hash ind in let htag = Int.hash tag in combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args) | MLint i -> @@ -545,7 +545,7 @@ let rec hash_mllambda gn n env t = | MLarray arr -> combinesmall 15 (hash_mllambda_array gn n env 1 arr) | MLisaccu (s, ind, c) -> - combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) + combinesmall 16 (combine (String.hash s) (combine (Ind.CanOrd.hash ind) (hash_mllambda gn n env c))) | MLfloat f -> combinesmall 17 (Float64.hash f) @@ -689,7 +689,7 @@ let eq_global g1 g2 = eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2 | Gopen s1, Gopen s2 -> String.equal s1 s2 | Gtype (ind1, arr1), Gtype (ind2, arr2) -> - eq_ind ind1 ind2 && + Ind.CanOrd.equal ind1 ind2 && Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2 | Gcomment s1, Gcomment s2 -> String.equal s1 s2 | _, _ -> false @@ -720,7 +720,7 @@ let hash_global g = let hash_aux acc (tag,ar) = combine3 acc (Int.hash tag) (Int.hash ar) in - combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr)) + combinesmall 6 (combine (Ind.CanOrd.hash ind) (Array.fold_left hash_aux 0 arr)) | Gcomment s -> combinesmall 7 (String.hash s) let global_stack = ref ([] : global list) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 00418009c7..76215b4386 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -80,7 +80,7 @@ and conv_atom env pb lvl a1 a2 cu = | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> - if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu + if Ind.CanOrd.equal ind1 ind2 then convert_instances ~flex:false u1 u2 cu else raise NotConvertible | Aconstant (c1,u1), Aconstant (c2,u2) -> if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu @@ -90,7 +90,7 @@ and conv_atom env pb lvl a1 a2 cu = | Avar id1, Avar id2 -> if Id.equal id1 id2 then cu else raise NotConvertible | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> - if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; + if not (Ind.CanOrd.equal a1.asw_ind a2.asw_ind) then raise NotConvertible; let cu = conv_accu env CONV lvl ac1 ac2 cu in let tbl = a1.asw_reloc in let len = Array.length tbl in @@ -124,7 +124,7 @@ and conv_atom env pb lvl a1 a2 cu = let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> - if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible + if not (Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 05c98e4b87..bd6241ae67 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -36,13 +36,13 @@ type annot_sw = { (* We compare only what is relevant for generation of ml code *) let eq_annot_sw asw1 asw2 = - eq_ind asw1.asw_ind asw2.asw_ind && + Ind.CanOrd.equal asw1.asw_ind asw2.asw_ind && String.equal asw1.asw_prefix asw2.asw_prefix open Hashset.Combine let hash_annot_sw asw = - combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix) + combine (Ind.CanOrd.hash asw.asw_ind) (String.hash asw.asw_prefix) type sort_annot = string * int diff --git a/kernel/primred.ml b/kernel/primred.ml index 17e5a89b74..f0b4d6d362 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -16,7 +16,7 @@ let check_same_types typ c1 c2 = then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2)) let check_same_inds ind i1 i2 = - if not (eq_ind i1 i2) + if not (Ind.CanOrd.equal i1 i2) then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2)) let add_retroknowledge retro action = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8eb1c10f70..5589ae3483 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -568,7 +568,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) -> - if eq_ind ind1 ind2 then + if Ind.CanOrd.equal ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -588,7 +588,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 then + if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -669,7 +669,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> - (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible); + (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible); let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in let ccnv = ccnv CONV l2r infos el1 el2 in let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in @@ -711,7 +711,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> - if not (eq_ind ci1.ci_ind ci2.ci_ind) then + if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible; let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 diff --git a/kernel/typeops.ml b/kernel/typeops.ml index f86c12e1f1..85e24f87b7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -413,7 +413,7 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_ind (Projection.inductive p) ind); + assert(Ind.CanOrd.equal (Projection.inductive p) ind); let ty = Vars.subst_instance_constr u pty in substl (c :: CList.rev args) ty diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2de902c827..1432fb9310 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -95,7 +95,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with | Aind ((mi,_i) as ind1) , Aind ind2 -> - if eq_ind ind1 ind2 && compare_stack stk1 stk2 then + if Ind.CanOrd.equal ind1 ind2 && compare_stack stk1 stk2 then let ulen = Univ.AUContext.size (Environ.mind_context env mi) in if ulen = 0 then conv_stack env k stk1 stk2 cu diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 28a7abc7c6..7b4101b9d0 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -96,7 +96,7 @@ let hash_structured_values (v : structured_values) = let eq_structured_constant c1 c2 = match c1, c2 with | Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 | Const_sort _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind i1, Const_ind i2 -> Ind.CanOrd.equal i1 i2 | Const_ind _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_b0 _, _ -> false @@ -113,7 +113,7 @@ let hash_structured_constant c = let open Hashset.Combine in match c with | Const_sort s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_ind i -> combinesmall 2 (Ind.CanOrd.hash i) | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l) | Const_val v -> combinesmall 5 (hash_structured_values v) diff --git a/library/coqlib.ml b/library/coqlib.ml index b374ecbca0..82d1ecacb5 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -45,7 +45,7 @@ let has_ref s = CString.Map.mem s !table let check_ind_ref s ind = match CString.Map.find s !table with - | GlobRef.IndRef r -> eq_ind r ind + | GlobRef.IndRef r -> Ind.CanOrd.equal r ind | _ -> false | exception Not_found -> false diff --git a/library/lib.ml b/library/lib.ml index 830777003b..d75177aaa9 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -525,7 +525,7 @@ let init () = let mp_of_global = let open GlobRef in function | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp | ConstRef cst -> Names.Constant.modpath cst - | IndRef ind -> Names.ind_modpath ind + | IndRef ind -> Names.Ind.modpath ind | ConstructRef constr -> Names.constr_modpath constr let rec dp_of_mp = function diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 23f8fe04a3..ac2058ba1b 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -115,7 +115,7 @@ module Bool = struct | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in - Names.eq_ind i (Lazy.force ind) + Names.Ind.CanOrd.equal i (Lazy.force ind) in if is_bool then Ifb ((aux arg), (aux pats.(0)), (aux pats.(1))) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index b1ce10985a..21ec80abbc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -685,7 +685,7 @@ let is_regular_match br = | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d464ec4c06..61f90608b1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -100,7 +100,7 @@ let rec make_form env sigma atom_env term = | Cast(a,_,_) -> make_form env sigma atom_env a | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_False)) then Bot else make_atom atom_env (normalize term) @@ -108,11 +108,11 @@ let rec make_form env sigma atom_env term = begin try let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_and)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then + else if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_or)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Disjunct (fa,fb) 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' diff --git a/tactics/elim.ml b/tactics/elim.ml index 49437a2aef..9a55cabc86 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -193,7 +193,7 @@ let head_in indl t gl = let sigma = Tacmach.New.project gl in try let ity,_ = extract_mrectype sigma t in - List.exists (fun i -> eq_ind (fst i) (fst ity)) indl + List.exists (fun i -> Ind.CanOrd.equal (fst i) (fst ity)) indl with Not_found -> false let decompose_these c l = diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index fee9dd1b96..df07dcbca7 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -91,7 +91,7 @@ struct | DArray (t,def,ty) -> DArray(Array.map f t, f def, f ty) let compare_ci ci1 ci2 = - let c = ind_ord ci1.ci_ind ci2.ci_ind in + let c = Ind.CanOrd.compare ci1.ci_ind ci2.ci_ind in if c = 0 then let c = Int.compare ci1.ci_npar ci2.ci_npar in if c = 0 then diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 475d4e9af9..f715459616 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let u,v = try destruct_ind env sigma tt1 (* trick so that the good sequence is returned*) with e when CErrors.noncritical e -> indu,[||] - in if eq_ind (fst u) ind + in if Ind.CanOrd.equal (fst u) ind then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ] else ( find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5f7eb78a40..bef9e29ac2 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id = let explain_wrong_case_info env (ind,u) ci = let pi = pr_inductive env ind in - if eq_ind ci.ci_ind ind then + if Ind.CanOrd.equal ci.ci_ind ind then str "Pattern-matching expression on an object of inductive type" ++ spc () ++ pi ++ spc () ++ str "has invalid information." else @@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i = pr_inductive env i ++ str "." let error_not_mutual_in_scheme env ind ind' = - if eq_ind ind ind' then + if Ind.CanOrd.equal ind ind' then str "The inductive type " ++ pr_inductive env ind ++ str " occurs twice." else diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index 79468627de..af72c01758 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms = | [], _::_ -> let () = match same_indccl with | ind :: _ -> - if List.distinct_f Names.ind_ord (List.map pi1 ind) + if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind) then Flags.if_verbose Feedback.msg_info (Pp.strbrk |