coq 8.7.2 · OCaml Package

module ArgT : sig ... end

type (!_, !_, !_) genarg_type =

| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
| ListArg : ('a0, 'b0, 'c0) genarg_type -> ('a0 list, 'b0 list, 'c0 list) genarg_type
| OptArg : ('a1, 'b1, 'c1) genarg_type -> ('a1 option, 'b1 option, 'c1 option) genarg_type
| 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 = [

]

type glevel = [

]

type tlevel = [

]

type (!_, !_) abstract_argument_type =

| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a0, 'b0, 'c0) genarg_type -> ('b0, glevel) abstract_argument_type
| 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 =

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 =

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.std_ppcmds

val genarg_tag : 'a generic_argument -> argument_type

val unquote : ('a, 'co) abstract_argument_type -> argument_type

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

package coq