package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Coq plugins are identified by their OCaml library name (in the Findlib sense)

type t

A plugin is identified by its canonical library name, such as coq-core.plugins.ltac

val repr : t -> string option * string

repr p returns a pair of legacy_name, lib_name where lib_name is the canoncial library name.

legacy_name may be Some pname for the cases the plugin was specified in Declare ML Module with their legacy name (for example ltac_plugin). This will stop being supported soon and is only here for compatiblity. Note that the name doesn't include the ".cmxs" / ".cma" extension

val pp : t -> string