package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.vernac/DeclareUniv/index.html

Module DeclareUnivSource

Sourceexception AlreadyDeclared of string option * Names.Id.t

Also used by Declare for constants, DeclareInd for inductives, etc. Containts object_kind , id.

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

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

Command Sort.