Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Univopen Sorts
type t = ElimConstraints.t * UnivConstraints.t
type pconstraints = t(** Stands for prenex sort poly constraints *)
val make : ElimConstraints.t -> UnivConstraints.t -> t
val empty : tval is_empty : t -> bool
val equal : t -> t -> bool
val qualities : t -> ElimConstraints.t
val univs : t -> UnivConstraints.t
val of_qualities : ElimConstraints.t -> t
val of_univs : UnivConstraints.t -> t
val set_qualities : ElimConstraints.t -> t -> t
val set_univs : UnivConstraints.t -> t -> t
val add_quality : ElimConstraint.t -> t -> t
val add_univ : UnivConstraint.t -> t -> t
val union : t -> t -> t
val diff : t -> t -> t
val elements : t -> ElimConstraint.t list * UnivConstraint.t list
val filter_qualities : (ElimConstraints.elt -> bool) -> t -> tval filter_univs : (UnivConstraints.elt -> bool) -> t -> t
val pr : Sorts.printer -> t -> Pp.t
val hcons : t Hashcons.f
type 'a constrained = 'a * t
val constraints_of : 'a constrained -> t
type 'a constraint_function = 'a -> 'a -> t -> t
val enforce_eq_univ : Level.t constraint_function
val enforce_leq_univ : Level.t constraint_function
val enforce_elim_to : Quality.t constraint_function
val fold : (ElimConstraint.t -> 'a -> 'a) * (UnivConstraint.t -> 'b -> 'b) -> t -> ('a * 'b) -> ('a * 'b)