Skip to content

Commit

Permalink
remove internal constraints alias in univ.ml
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Sep 7, 2023
1 parent 4a0f604 commit ef29b60
Showing 1 changed file with 3 additions and 5 deletions.
8 changes: 3 additions & 5 deletions kernel/univ.ml
Original file line number Diff line number Diff line change
Expand Up @@ -506,8 +506,6 @@ struct

end

type constraints = Constraints.t

module Hconstraint =
Hashcons.Make(
struct
Expand All @@ -522,7 +520,7 @@ module Hconstraint =
module Hconstraints =
Hashcons.Make(
struct
type t = constraints
type t = Constraints.t
type u = univ_constraint -> univ_constraint
let hashcons huc s =
Constraints.fold (fun x -> Constraints.add (huc x)) s Constraints.empty
Expand All @@ -538,13 +536,13 @@ let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate Hconstraints


(** A value with universe constraints. *)
type 'a constrained = 'a * constraints
type 'a constrained = 'a * Constraints.t

let constraints_of (_, cst) = cst

(** Constraints functions. *)

type 'a constraint_function = 'a -> 'a -> constraints -> constraints
type 'a constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t

let enforce_eq_level u v c =
(* We discard trivial constraints like u=u *)
Expand Down

0 comments on commit ef29b60

Please sign in to comment.