package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a pervasives_ref = 'a ref
val pervasives_ref : 'a -> 'a ref
val pervasives_compare : 'a -> 'a -> int
val (!) : 'a ref -> 'a
val (+) : int -> int -> int
val (-) : int -> int -> int
val on_fst : ('a -> 'b) -> ('a * 'c) -> 'b * 'c
val on_snd : ('a -> 'b) -> ('c * 'a) -> 'c * 'b
val map_pair : ('a -> 'b) -> ('a * 'a) -> 'b * 'b
val on_pi1 : ('a -> 'b) -> ('a * 'c * 'd) -> 'b * 'c * 'd
val on_pi2 : ('a -> 'b) -> ('c * 'a * 'd) -> 'c * 'b * 'd
val on_pi3 : ('a -> 'b) -> ('c * 'd * 'a) -> 'c * 'd * 'b
val pi1 : ('a * 'b * 'c) -> 'a
val pi2 : ('a * 'b * 'c) -> 'b
val pi3 : ('a * 'b * 'c) -> 'c
val is_letter : char -> bool
val is_digit : char -> bool
val is_ident_tail : char -> bool
val is_blank : char -> bool
module Empty : sig ... end
val subst_command_placeholder : string -> string -> string
module List : CList.ExtS
val (@) : 'a list -> 'a list -> 'a list
module Set : sig ... end
module Map : sig ... end
val stream_nth : int -> 'a Stream.t -> 'a
val stream_njunk : int -> 'a Stream.t -> unit
val matrix_transpose : 'a list list -> 'a list list
val identity : 'a -> 'a
val (%>) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
val const : 'a -> 'b -> 'a
val iterate : ('a -> 'a) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
val app_opt : ('a -> 'a) option -> 'a -> 'a
type !'a delayed = unit -> 'a
val delayed_force : 'a delayed -> 'a
val try_finally : ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b
type iexn = Exninfo.iexn
  • deprecated please use [Exninfo.iexn]
val iraise : Exninfo.iexn -> 'a
  • deprecated please use [Exninfo.iraise]
type (!'a, !'b) union = ('a, 'b) CSig.union =
  1. | Inl of 'a
  2. | Inr of 'b
module Union : sig ... end
val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
type !'a until = 'a CSig.until =
  1. | Stop of 'a
  2. | Cont of 'a
type (!'a, !'b) eq = ('a, 'b) CSig.eq =
  1. | Refl : ('a0, 'a0) eq
val sym : ('a, 'b) eq -> ('b, 'a) eq
val open_utf8_file_in : string -> in_channel
val set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a)