Coqlib (rocq-runtime.Coqlib)

include module type of struct include Rocqlib end

val register_ref : Libobject.locality -> string -> Names.GlobRef.t -> unit

Registers a global reference under the given name.

exception NotFoundRef of string

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

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

As lib_ref but returns None instead of raising.

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

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

Checks whether a name is bound to a known reference.

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

Checks whether a name is bound to a known inductive.

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

List of all currently bound names.

For Equality tactics

type rocq_sigma_data = Rocqlib.rocq_sigma_data = {

proj1 : Names.GlobRef.t;

proj2 : Names.GlobRef.t;

elim : Names.GlobRef.t;

intro : Names.GlobRef.t;

typ : Names.GlobRef.t;

}

val build_sigma_type : rocq_sigma_data Util.delayed

val build_sigma : rocq_sigma_data Util.delayed

val build_prod : rocq_sigma_data Util.delayed

type rocq_eq_data = Rocqlib.rocq_eq_data = {

eq : Names.GlobRef.t;

ind : Names.GlobRef.t;

refl : Names.GlobRef.t;

sym : Names.GlobRef.t;

trans : Names.GlobRef.t;

congr : Names.GlobRef.t;

}

val build_rocq_eq_data : rocq_eq_data Util.delayed

val build_rocq_identity_data : rocq_eq_data Util.delayed

val build_rocq_jmeq_data : rocq_eq_data Util.delayed

val check_required_library : string list -> unit

For tactics/commands requiring vernacular libraries

val datatypes_module_name : string list

val logic_module_name : string list

val jmeq_module_name : string list

type coq_sigma_data = rocq_sigma_data = {