package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CoqlibSource

Deprecated alias for Rocqlib

  • deprecated (9.0) Use Rocqlib
include module type of struct include Rocqlib end
Sourceval register_ref : Libobject.locality -> string -> Names.GlobRef.t -> unit

Registers a global reference under the given name.

Sourceexception NotFoundRef of string
Sourceval lib_ref : string -> Names.GlobRef.t

Retrieves the reference bound to the given name (by a previous call to register_ref). Raises NotFoundRef if no reference is bound to this name.

Sourceval lib_ref_opt : string -> Names.GlobRef.t option

As lib_ref but returns None instead of raising.

Sourceval has_ref : string -> bool

Checks whether a name refers to a registered constant. For any name n, if has_ref n returns true, lib_ref n will succeed.

Sourceval check_ref : string -> Names.GlobRef.t -> bool

Checks whether a name is bound to a known reference.

Sourceval check_ind_ref : string -> Names.inductive -> bool

Checks whether a name is bound to a known inductive.

Sourceval get_lib_refs : unit -> (string * Names.GlobRef.t) list

List of all currently bound names.

For Equality tactics

Sourcetype rocq_sigma_data = Rocqlib.rocq_sigma_data = {
  1. proj1 : Names.GlobRef.t;
  2. proj2 : Names.GlobRef.t;
  3. elim : Names.GlobRef.t;
  4. intro : Names.GlobRef.t;
  5. typ : Names.GlobRef.t;
}
Sourceval build_sigma_type : rocq_sigma_data Util.delayed
Sourceval build_rocq_eq_data : rocq_eq_data Util.delayed
Sourceval build_rocq_identity_data : rocq_eq_data Util.delayed
Sourceval build_rocq_jmeq_data : rocq_eq_data Util.delayed
Sourceval check_required_library : string list -> unit

For tactics/commands requiring vernacular libraries

Sourceval datatypes_module_name : string list
Sourceval logic_module_name : string list
Sourceval jmeq_module_name : string list
Sourcetype coq_sigma_data = rocq_sigma_data = {
  1. proj1 : Names.GlobRef.t;
  2. proj2 : Names.GlobRef.t;
  3. elim : Names.GlobRef.t;
  4. intro : Names.GlobRef.t;
  5. typ : Names.GlobRef.t;
}
  • deprecated (9.0) Use Rocqlib.rocq_sigma_data
  • deprecated (9.0) Use Rocqlib.rocq_eq_data
Sourceval build_coq_eq_data : rocq_eq_data Util.delayed
  • deprecated (9.0) Use Rocqlib.build_rocq_eq_data
Sourceval build_coq_identity_data : rocq_eq_data Util.delayed
  • deprecated (9.0) Use Rocqlib.build_rocq_identity_data
Sourceval build_coq_jmeq_data : rocq_eq_data Util.delayed
  • deprecated (9.0) Use Rocqlib.build_rocq_jmeq_data
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct