package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module ArgT : sig ... end
type (!_, !_, !_) genarg_type =
  1. | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
  2. | ListArg : ('a0, 'b0, 'c0) genarg_type -> ('a0 list, 'b0 list, 'c0 list) genarg_type
  3. | OptArg : ('a1, 'b1, 'c1) genarg_type -> ('a1 option, 'b1 option, 'c1 option) genarg_type
  4. | PairArg : ('a10, 'b10, 'c10) genarg_type * ('a2, 'b2, 'c2) genarg_type -> ('a10 * 'a2, 'b10 * 'b2, 'c10 * 'c2) genarg_type
type !'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
val make0 : string -> ('raw, 'glob, 'top) genarg_type
val create_arg : string -> ('raw, 'glob, 'top) genarg_type
type rlevel = [
  1. | `rlevel
]
type glevel = [
  1. | `glevel
]
type tlevel = [
  1. | `tlevel
]
type (!_, !_) abstract_argument_type =
  1. | Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
  2. | Glbwit : ('a0, 'b0, 'c0) genarg_type -> ('b0, glevel) abstract_argument_type
  3. | Topwit : ('a1, 'b1, 'c1) genarg_type -> ('c1, tlevel) abstract_argument_type
type !'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
type !'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type
type !'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type
val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
type !'l0 generic_argument =
  1. | GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument
val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a
val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
type argument_type =
  1. | ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
val argument_type_eq : argument_type -> argument_type -> bool
val genarg_type_eq : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
val abstract_argument_type_eq : ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> ('a, 'b) CSig.eq option
val pr_argument_type : argument_type -> Pp.t
val genarg_tag : 'a generic_argument -> argument_type
val unquote : ('a, 'co) abstract_argument_type -> argument_type
val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag
module type GenObj = sig ... end
module Register (M : GenObj) : sig ... end
val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type