Coqlib (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.rocq-runtime.library.Coqlib)

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.

Sourcetype rocq_sigma_data = Rocqlib.rocq_sigma_data = {

}

Sourceval build_sigma_type : rocq_sigma_data Util.delayed

Sourceval build_sigma : rocq_sigma_data Util.delayed

Sourceval build_prod : rocq_sigma_data Util.delayed

Sourcetype rocq_eq_data = Rocqlib.rocq_eq_data = {

}

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 = {

}

Sourcetype coq_eq_data = rocq_eq_data = {

}

Sourceval build_coq_eq_data : rocq_eq_data Util.delayed

Sourceval build_coq_identity_data : rocq_eq_data Util.delayed

Sourceval build_coq_jmeq_data : rocq_eq_data Util.delayed