aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml6
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/inductive.ml6
-rw-r--r--kernel/names.ml1
-rw-r--r--kernel/names.mli16
-rw-r--r--kernel/nativecode.ml8
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/primred.ml2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/vmemitcodes.ml4
-rw-r--r--kernel/vmvalues.ml4
12 files changed, 31 insertions, 24 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 1837a39764..fb1e4d12da 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -353,7 +353,7 @@ let isRef c = match kind c with
let isRefX x c =
let open GlobRef in
match x, kind c with
- | ConstRef c, Const (c', _) -> Constant.equal c c'
+ | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
| IndRef i, Ind (i', _) -> eq_ind i i'
| ConstructRef i, Construct (i', _) -> eq_constructor i i'
| VarRef id, Var id' -> Id.equal id id'
@@ -954,7 +954,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
| Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
| Const (c1,u1), Const (c2,u2) ->
(* The args length currently isn't used but may as well pass it. *)
- Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2
+ 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
| Construct (c1,u1), Construct (c2,u2) ->
eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
@@ -1442,7 +1442,7 @@ let rec hash t =
| Evar (e,l) ->
combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
| Const (c,u) ->
- combinesmall 9 (combine (Constant.hash c) (Instance.hash u))
+ combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u))
| Ind (ind,u) ->
combinesmall 10 (combine (ind_hash ind) (Instance.hash u))
| Construct (c,u) ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index b9f434f179..ee90ad382b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -159,7 +159,7 @@ let hcons_const_body cb =
let eq_nested_type t1 t2 = match t1, t2 with
| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2
| NestedInd _, _ -> false
-| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2
| NestedPrimitive _, _ -> false
let eq_recarg r1 r2 = match r1, r2 with
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d751d9875a..2b1a295620 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -472,7 +472,7 @@ let inter_recarg r1 r2 = match r1, r2 with
| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
| Nested (NestedInd _), _ -> None
| Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) ->
- if Names.Constant.equal c1 c2 then Some r1 else None
+ if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None
| Nested (NestedPrimitive _), _ -> None
let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec
@@ -644,7 +644,7 @@ let abstract_mind_lc ntyps npars lc =
let is_primitive_positive_container env c =
match env.retroknowledge.Retroknowledge.retro_array with
- | Some c' when Constant.equal c c' -> true
+ | Some c' when QConstant.equal env c c' -> true
| _ -> false
(* [get_recargs_approx env tree ind args] builds an approximation of the recargs
@@ -673,7 +673,7 @@ let get_recargs_approx env tree ind args =
end
| Const (c,_) when is_primitive_positive_container env c ->
begin match dest_recarg tree with
- | Nested (NestedPrimitive c') when Constant.equal c c' ->
+ | Nested (NestedPrimitive c') when QConstant.equal env c c' ->
build_recargs_nested_primitive ienv tree (c, largs)
| _ -> mk_norec
end
diff --git a/kernel/names.ml b/kernel/names.ml
index 592b5e65f7..f987b1d92e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -529,6 +529,7 @@ module KerPair = struct
end
module SyntacticOrd = struct
+ type t = kernel_pair
let compare x y = match x, y with
| Same knx, Same kny -> KerName.compare knx kny
| Dual (knux,kncx), Dual (knuy,kncy) ->
diff --git a/kernel/names.mli b/kernel/names.mli
index ea137ad1f4..9a01ea2b43 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -341,27 +341,30 @@ sig
(** Comparisons *)
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
- val equal : t -> t -> bool
+ val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"]
(** Default comparison, alias for [CanOrd.equal] *)
- val hash : t -> int
+ val hash : t -> int [@@ocaml.deprecated "Use QConstant.hash"]
(** Hashing function *)
val change_label : t -> Label.t -> t
@@ -431,27 +434,30 @@ sig
(** Comparisons *)
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
- val equal : t -> t -> bool
- (** Default comparison, alias for [CanOrd.equal] *)
+ val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"]
+ (** Default comparison, alias for [CanOrd.equal] *)
- val hash : t -> int
+ val hash : t -> int [@@ocaml.deprecated "Use QMutInd.hash"]
(** Displaying *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ae070e6f8e..9314203e04 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -67,7 +67,7 @@ let eq_gname gn1 gn2 =
| Gind (s1, ind1), Gind (s2, ind2) ->
String.equal s1 s2 && eq_ind ind1 ind2
| Gconstant (s1, c1), Gconstant (s2, c2) ->
- String.equal s1 s2 && Constant.equal c1 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
| Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2
@@ -98,7 +98,7 @@ let gname_hash gn = match gn with
| Gind (s, ind) ->
combinesmall 1 (combine (String.hash s) (ind_hash ind))
| Gconstant (s, c) ->
- combinesmall 2 (combine (String.hash s) (Constant.hash 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))
| Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
| Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
@@ -148,7 +148,7 @@ let eq_symbol sy1 sy2 =
| SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *)
| SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2
| SymbName n1, SymbName n2 -> Name.equal n1 n2
- | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
+ | 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
| SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
@@ -162,7 +162,7 @@ let hash_symbol symb =
| SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *)
| SymbSort s -> combinesmall 2 (Sorts.hash s)
| SymbName name -> combinesmall 3 (Name.hash name)
- | SymbConst c -> combinesmall 4 (Constant.hash c)
+ | SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c)
| SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
| SymbInd ind -> combinesmall 6 (ind_hash ind)
| SymbMeta m -> combinesmall 7 m
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index fc6afb79d4..00418009c7 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -83,7 +83,7 @@ and conv_atom env pb lvl a1 a2 cu =
if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
else raise NotConvertible
| Aconstant (c1,u1), Aconstant (c2,u2) ->
- if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+ if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
else raise NotConvertible
| Asort s1, Asort s2 ->
sort_cmp_universes env pb s1 s2 cu
diff --git a/kernel/primred.ml b/kernel/primred.ml
index f158cfacea..17e5a89b74 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -12,7 +12,7 @@ type _ action_kind =
type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
let check_same_types typ c1 c2 =
- if not (Constant.equal c1 c2)
+ if not (Constant.CanOrd.equal c1 c2)
then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
let check_same_inds ind i1 i2 =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 96bf370342..f295b36b60 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -283,7 +283,7 @@ let convert_constructors ctor nargs u1 u2 (s, check) =
let conv_table_key infos k1 k2 cuniv =
if k1 == k2 then cuniv else
match k1, k2 with
- | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
+ | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' ->
if Univ.Instance.equal u u' then cuniv
else
let flex = evaluable_constant cst (info_env infos)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 76a1c190be..1a4c786e43 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -182,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
begin
let kn2' = kn_of_delta reso2 kn2 in
if KerName.equal kn2 kn2' ||
- MutInd.equal (mind_of_delta_kn reso1 kn1)
+ MutInd.CanOrd.equal (mind_of_delta_kn reso1 kn1)
(subst_mind subst2 (MutInd.make kn2 kn2'))
then ()
else error NotEqualInductiveAliases
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index ec8601edc9..42908a7363 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -36,7 +36,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with
| Reloc_annot _, _ -> false
| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2
| Reloc_const _, _ -> false
-| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
+| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2
| Reloc_getglobal _, _ -> false
| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
| Reloc_proj_name _, _ -> false
@@ -48,7 +48,7 @@ let hash_reloc_info r =
match r with
| Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
| Reloc_const c -> combinesmall 2 (hash_structured_constant c)
- | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+ | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c)
| Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
| Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 2068133b10..28a7abc7c6 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -250,7 +250,7 @@ type id_key =
| EvarKey of Evar.t
let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with
-| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2
+| ConstKey c1, ConstKey c2 -> Constant.CanOrd.equal c1 c2
| VarKey id1, VarKey id2 -> Id.equal id1 id2
| RelKey n1, RelKey n2 -> Int.equal n1 n2
| EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2
@@ -469,7 +469,7 @@ struct
let equal = eq_id_key
open Hashset.Combine
let hash : t -> tag = function
- | ConstKey c -> combinesmall 1 (Constant.hash c)
+ | ConstKey c -> combinesmall 1 (Constant.CanOrd.hash c)
| VarKey id -> combinesmall 2 (Id.hash id)
| RelKey i -> combinesmall 3 (Int.hash i)
| EvarKey evk -> combinesmall 4 (Evar.hash evk)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:42:23 +0000