package coq-core

  1. Overview
  2. Docs
On This Page
  1. Locate
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

A Pretty-Printer for the Calculus of Inductive Constructions.

val assumptions_for_print : Names.Name.t list -> Termops.names_context
val print_closed_sections : bool Stdlib.ref
val print_context : Environ.env -> Evd.evar_map -> bool -> int option -> 'a Lib.library_segment -> Pp.t
val print_library_leaf : Environ.env -> Evd.evar_map -> bool -> Names.ModPath.t -> Libobject.t -> Pp.t option
val print_library_node : Summary.Interp.frozen Lib.node -> Pp.t
val print_full_context : Environ.env -> Evd.evar_map -> Pp.t
val print_full_context_typ : Environ.env -> Evd.evar_map -> Pp.t
val print_full_pure_context : Environ.env -> Evd.evar_map -> Pp.t
val print_sec_context : Environ.env -> Evd.evar_map -> Libnames.qualid -> Pp.t
val print_sec_context_typ : Environ.env -> Evd.evar_map -> Libnames.qualid -> Pp.t
val print_safe_judgment : Safe_typing.judgment -> Pp.t
val print_notation : Environ.env -> Evd.evar_map -> Constrexpr.notation_entry -> string -> Pp.t
val print_abbreviation : Environ.env -> Names.KerName.t -> Pp.t
val print_impargs : Names.GlobRef.t -> Pp.t
val print_graph : unit -> Pp.t

Pretty-printing functions for classes and coercions

val print_classes : unit -> Pp.t
val print_coercions : unit -> Pp.t
val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
val print_canonical_projections : Environ.env -> Evd.evar_map -> Names.GlobRef.t list -> Pp.t
val print_typeclasses : unit -> Pp.t

Pretty-printing functions for type classes and instances

val print_instances : Names.GlobRef.t -> Pp.t
val print_all_instances : unit -> Pp.t
val inspect : Environ.env -> Evd.evar_map -> int -> Pp.t
Locate
type 'a locatable_info = {
  1. locate : Libnames.qualid -> 'a option;
    (*

    Locate the most precise object with the provided name if any.

    *)
  2. locate_all : Libnames.qualid -> 'a list;
    (*

    Locate all objects whose name is a suffix of the provided name

    *)
  3. shortest_qualid : 'a -> Libnames.qualid;
    (*

    Return the shortest name in the current context

    *)
  4. name : 'a -> Pp.t;
    (*

    Data as printed by the Locate command

    *)
  5. print : 'a -> Pp.t;
    (*

    Data as printed by the Print command

    *)
  6. about : 'a -> Pp.t;
    (*

    Data as printed by the About command

    *)
}

Generic data structure representing locatable objects.

val register_locatable : string -> 'a locatable_info -> unit

Define a new type of locatable objects that can be reached via the corresponding generic vernacular commands. The string should be a unique name describing the kind of objects considered and that is added as a grammar command prefix for vernacular commands Locate.

val print_located_qualid : Libnames.qualid -> Pp.t
val print_located_term : Libnames.qualid -> Pp.t
val print_located_module : Libnames.qualid -> Pp.t
val print_located_other : string -> Libnames.qualid -> Pp.t
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