Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243(************************************************************************)(* * 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) *)(************************************************************************)
type t(** Set of flags for universe polymorphism, implicit sort polymorphism and cumulativity. Note that implicit sort polymorphism (not collapsing sort variables to Type) and cumulativity only make sense for constructions that are already polymorphic. This invariant is ensured by the smart constructor below. *)
(** Raises a user error if [univ_poly = false] and either [collapse_sort_variables = false] or [cumulative = true]. *)val make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> t
(** The [default] is monomorphic: [univ_poly] and [cumulative] are [false], [collapse_sort_variables] is [true] *)val default : t
(** Only sets the universe [univ_poly] flag. Use with care, this probably indicates that the code does not handle [cumulative] constructions when it should. Code relying on elaboration should also support the [collapse_sort_variables] flag. *)val of_univ_poly : bool -> t
(** Accessors *)val univ_poly : t -> boolval collapse_sort_variables : t -> boolval cumulative : t -> bool
(** Pretty print *)val pr : t -> Pp.t
(** Used to have distinguished default behaviors when treating assumptions/axioms, definitions or inductives *)type construction_kind = Assumption | Definition | Inductive