DeclareUniv
exception AlreadyDeclared of string option * Names.Id.t
Also used by Declare
for constants, DeclareInd
for inductives, etc. Containts object_kind , id
.
val declare_univ_binders : Names.GlobRef.t -> UState.named_universes_entry -> unit
Internally used to declare names of universes from monomorphic constants/inductives. Noop on polymorphic references.
val do_universe : poly:bool -> Names.lident list -> unit
Command Universes
.
val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
Command Constraint
.