package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Extraction_plugin.CommonSource

By default, in module Format, you can do horizontal placing of blocks even if they include newlines, as long as the number of chars in the blocks are less that a line length. To avoid this awkward situation, we attach a big virtual size to fnl newlines.

Sourceval fnl : unit -> Pp.t
Sourceval fnl2 : unit -> Pp.t
Sourceval space_if : bool -> Pp.t
Sourceval pp_par : bool -> Pp.t -> Pp.t
Sourceval pp_apply : Pp.t -> bool -> Pp.t list -> Pp.t

pp_apply : a head part applied to arguments, possibly with parenthesis

Sourceval pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t

Same as pp_apply, but with also protection of the head by parenthesis

Sourceval pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
Sourceval pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
Sourceval pp_array : ('a -> Pp.t) -> 'a list -> Pp.t
Sourceval pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
Sourceval pr_binding : Names.Id.t list -> Pp.t
Sourceval empty_env : unit -> env
Sourceval rename_vars : Names.Id.Set.t -> Names.Id.t list -> env
Sourceval rename_tvars : Names.Id.Set.t -> Names.Id.t list -> Names.Id.t list
Sourceval push_vars : Names.Id.t list -> env -> Names.Id.t list * env
Sourceval get_db_name : int -> env -> Names.Id.t
Sourcetype phase =
  1. | Pre
  2. | Impl
  3. | Intf
Sourceval set_phase : phase -> unit
Sourceval get_phase : unit -> phase
Sourceval opened_libraries : unit -> Names.ModPath.t list
Sourcetype kind =
  1. | Term
  2. | Type
  3. | Cons
  4. | Mod
Sourceval pp_global : kind -> Names.GlobRef.t -> string
Sourceval pp_global_name : kind -> Names.GlobRef.t -> string
Sourceval pp_module : Names.ModPath.t -> string
Sourceval top_visible_mp : unit -> Names.ModPath.t
Sourceval push_visible : Names.ModPath.t -> Names.ModPath.t list -> unit
Sourceval pop_visible : unit -> unit
Sourceval get_duplicate : Names.ModPath.t -> Names.Label.t -> string option
Sourcetype reset_kind =
  1. | AllButExternal
  2. | Everything
Sourceval reset_renaming_tables : reset_kind -> unit
Sourceval set_keywords : Names.Id.Set.t -> unit

Special hack for constants of type Ascii.ascii : if an Extract Inductive ascii => char has been declared, then the constants are directly turned into chars

Sourceval is_native_char : Miniml.ml_ast -> bool
Sourceval get_native_char : Miniml.ml_ast -> char
Sourceval pp_native_char : Miniml.ml_ast -> Pp.t

Special hack for constants of type String.string : if an Extract Inductive string => string has been declared, then the constants are directly turned into string literals

Sourceval is_native_string : Miniml.ml_ast -> bool
Sourceval get_native_string : Miniml.ml_ast -> string
Sourceval pp_native_string : Miniml.ml_ast -> Pp.t
Sourceval sig_type_ref : unit -> Names.GlobRef.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct