package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

exception Unsupported of string

val current_decl_name : string ref

module C : sig ... end

type info = {

env : Env.env;
prelude : Printer.prelude;
thprelude : Printer.prelude_map;
thinterface : Printer.interface_map;
blacklist : Printer.blacklist;
syntax : Printer.syntax_map;
literal : Printer.syntax_map;
kn : Pdecl.known_map;
prec : int list Ident.Mid.t;

}

val debug_c_extraction : Debug.flag

val debug_c_no_error_msgs : Debug.flag

module Print : sig ... end

module MLToC : sig ... end

val name_gen : string -> ?fname:string -> Pmodule.pmodule -> string

val header_border_printer : 
  bool ->
  'a ->
  ?old:'b ->
  ?fname:string ->
  flat:'c ->
  Format.formatter ->
  Pmodule.pmodule ->
  unit

val mk_info : Pdriver.printer_args -> Pmodule.pmodule -> info

val print_header_decl : 
  Pdriver.printer_args ->
  ?old:in_channel ->
  ?fname:string ->
  flat:bool ->
  Pmodule.pmodule ->
  Format.formatter ->
  Mltree.decl ->
  unit

val print_prelude : 
  'a ->
  ?old:'b ->
  ?fname:'c ->
  flat:'d ->
  Pmodule.pmodule list ->
  Format.formatter ->
  'e ->
  unit

val print_decl : 
  Pdriver.printer_args ->
  ?old:in_channel ->
  ?fname:string ->
  flat:bool ->
  Pmodule.pmodule ->
  Format.formatter ->
  Mltree.decl ->
  unit

val c_printer : Pdriver.printer