package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

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 name_mono_section_univs : Univ.Level.Set.t -> unit

Internally used to name universes associated with no particular constant in a section.

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

Command Universes.

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

Command Constraint.

Sourceval add_constraint_source : Names.GlobRef.t -> Univ.ContextSet.t -> unit

Sourceval constraint_sources : unit -> (Names.GlobRef.t * Univ.Constraints.t) list

Returns constraints associated to globrefs, newest first.