matita/components/ng_extraction/coq.mli

   1 type identifier = string
   2
   3 val next_ident_away : identifier -> identifier list -> identifier
   4
   5 val lift_subscript   : identifier -> identifier
   6
   7 type label
   8 type reference
   9
  10 type env
  11 type constant_body
  12 type ('a,'b) prec_declaration
  13
  14 type module_path
  15 type mod_bound_id
  16
  17 module Intmap : Map.S with type key = int
  18
  19 module Intset : Set.S with type elt = int
  20
  21 module Uriset : Set.S with type elt = NUri.uri
  22
  23 module Idset : Set.S with type elt=identifier
  24
  25 module Refmap : Map.S with type key = NReference.reference
  26
  27 module Stringmap : Map.S with type key = string
  28
  29 module Pp_control : sig
  30  val with_output_to : out_channel -> Format.formatter
  31  val get_margin: unit -> int option
  32 end
  33
  34 val iterate : ('a -> 'a) -> int -> 'a -> 'a
  35 val list_skipn : int -> 'a list -> 'a list
  36 val list_split_at : int -> 'a list -> 'a list*'a list
  37 val list_chop : int -> 'a list -> 'a list * 'a list
  38 val list_firstn : int -> 'a list -> 'a list
  39 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
  40 val list_lastn : int -> 'a list -> 'a list
  41 val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
  42 val array_for_all : ('a -> bool) -> 'a array -> bool
  43 val array_fold_right_i :
  44   (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
  45 val identity : 'a -> 'a
  46 val interval : int -> int -> int list
  47 val map_status: 's -> ('s -> 'a -> 's * 'b) -> 'a list -> 's * 'b list
  48 val array_map_status: 's -> ('s -> 'a -> 's * 'b) -> 'a array -> 's * 'b array
  49 val array_mapi_status :
  50  's -> ('s -> int -> 'a -> 's * 'b) -> 'a array -> 's * 'b array
  51
  52 type std_ppcmds
  53 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
  54 val spc : unit -> std_ppcmds
  55 val str : string -> std_ppcmds
  56 val mt : unit -> std_ppcmds
  57 val v : int -> std_ppcmds -> std_ppcmds
  58 val hv : int -> std_ppcmds -> std_ppcmds
  59 val hov : int -> std_ppcmds -> std_ppcmds
  60 val int : int -> std_ppcmds
  61 val stras : int * string -> std_ppcmds
  62 val fnl : unit -> std_ppcmds
  63 val prlist_with_sep_status :
  64  'a -> (unit -> std_ppcmds) -> ('a -> 'b -> 'a * std_ppcmds) -> 'b list ->
  65    'a * std_ppcmds
  66 val prlist_with_sep :
  67    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
  68 val pr_id : identifier -> std_ppcmds
  69 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
  70 val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
  71 val prvect_with_sep :
  72    (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
  73 val prvect_with_sep_status :
  74  's -> (unit -> std_ppcmds) -> ('s -> 'a -> 's * std_ppcmds) -> 'a array -> 's * std_ppcmds
  75 val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
  76 val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
  77 val prvecti_status :
  78  's -> ('s -> int -> 'a -> 's * std_ppcmds) -> 'a array -> 's * std_ppcmds
  79 val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
  80 val list_map_i_status :
  81  's -> ('s -> int -> 'a -> 's * 'b) -> int -> 'a list -> 's * 'b list
  82
  83 val pp_with : Format.formatter -> std_ppcmds -> unit