Module `Extraction_plugin.Common`Source

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 rename_id : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Sourcetype env = Names.Id.t list * Names.Id.Set.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 =

| Pre
| Impl
| Intf

Sourceval set_phase : phase -> unit

Sourceval get_phase : unit -> phase

Sourceval opened_libraries : unit -> Names.ModPath.t list

Sourcetype kind =

| Term
| Type
| Cons
| Mod

Sourceval pp_global_with_key : kind -> Names.KerName.t -> Names.GlobRef.t -> string

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 =

| AllButExternal
| 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Common/index.html

Module `Extraction_plugin.Common`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Common/index.html

Module Extraction_plugin.CommonSource

Module `Extraction_plugin.Common`Source