package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

md5=5d1187d5e44ed0163f76fb12dabf012e

sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

Sourceexception 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.

Sourceval do_universe : poly:bool -> Names.lident list -> unit

Command Universes.

Sourceval do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit

Command Constraint.