PConstraints (p.rocq-runtime.9.2.0.doc.rocq-runtime.kernel.PConstraints)

Sourcetype t = Sorts.ElimConstraints.t * Univ.UnivConstraints.t

Sourcetype pconstraints = t

Stands for prenex sort poly constraints

Sourceval make : Sorts.ElimConstraints.t -> Univ.UnivConstraints.t -> t

Sourceval empty : t

Sourceval is_empty : t -> bool

Sourceval equal : t -> t -> bool

Sourceval qualities : t -> Sorts.ElimConstraints.t

Sourceval univs : t -> Univ.UnivConstraints.t

Sourceval of_qualities : Sorts.ElimConstraints.t -> t

Sourceval of_univs : Univ.UnivConstraints.t -> t

Sourceval set_qualities : Sorts.ElimConstraints.t -> t -> t

Sourceval set_univs : Univ.UnivConstraints.t -> t -> t

Sourceval add_quality : Sorts.ElimConstraint.t -> t -> t

Sourceval add_univ : Univ.UnivConstraint.t -> t -> t

Sourceval union : t -> t -> t

Sourceval diff : t -> t -> t

Sourceval elements : t -> Sorts.ElimConstraint.t list * Univ.UnivConstraint.t list

Sourceval filter_qualities : (Sorts.ElimConstraints.elt -> bool) -> t -> t

Sourceval filter_univs : (Univ.UnivConstraints.elt -> bool) -> t -> t

Sourceval pr : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> t -> Pp.t

Sourceval hcons : t Hashcons.f

Sourcetype 'a constrained = 'a * t

Sourceval constraints_of : 'a constrained -> t

Sourcetype 'a constraint_function = 'a -> 'a -> t -> t

Sourceval enforce_eq_univ : Univ.Level.t constraint_function

Sourceval enforce_leq_univ : Univ.Level.t constraint_function

Sourceval enforce_elim_to : Sorts.Quality.t constraint_function

val fold : 
  ((Sorts.ElimConstraint.t -> 'a -> 'a) * (Univ.UnivConstraint.t -> 'b -> 'b)) ->
  t ->
  ('a * 'b) ->
  'a * 'b