Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041(************************************************************************)(* * 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 = { univ_poly : bool; collapse_sort_variables : bool; cumulative : bool;}
let make ~univ_poly ~collapse_sort_variables ~cumulative = if cumulative && not univ_poly then CErrors.user_err Pp.(str "Cannot have cumulative but not universe polymorphic constructions"); if not collapse_sort_variables && not univ_poly then CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions"); { collapse_sort_variables; univ_poly; cumulative }
let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false }let of_univ_poly b = { default with univ_poly = b }
let collapse_sort_variables x = x.collapse_sort_variableslet univ_poly x = x.univ_polylet cumulative x = x.cumulative
let pr f = let open Pp in str "{ univ_poly = " ++ bool f.univ_poly ++ spc () ++ str "; cumulative = " ++ bool f.cumulative ++ spc () ++ str "; collapse_sort_variables = " ++ bool f.collapse_sort_variables ++ spc () ++ str "}"
(* Used to have distinguished default behaviors when treating assumptions/axioms, definitions or inductives *)type construction_kind = Assumption | Definition | Inductive