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 Jul 10, 2023
1 parent db10471 commit c42e9f2
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 @@ -513,8 +513,6 @@ struct

end

type constraints = Constraints.t

module Hconstraint =
Hashcons.Make(
struct
Expand All @@ -529,7 +527,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 @@ -545,13 +543,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 c42e9f2

Please sign in to comment.