Module Extraction_plugin.Common

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

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

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

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

val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
val pr_binding : Names.Id.t list -> Pp.t
val rename_id : Names.Id.t -> Names.Id.Set.t -> Names.Id.t
type env = Names.Id.t list * Names.Id.Set.t
val empty_env : unit -> env
val rename_vars : Names.Id.Set.t -> Names.Id.t list -> env
val rename_tvars : Names.Id.Set.t -> Names.Id.t list -> Names.Id.t list
val push_vars : Names.Id.t list -> env -> Names.Id.t list * env
val get_db_name : int -> env -> Names.Id.t
type phase =
| Pre
| Impl
| Intf
val set_phase : phase -> unit
val get_phase : unit -> phase
val opened_libraries : unit -> Names.ModPath.t list
type kind =
| Term
| Type
| Cons
| Mod
val pp_global : kind -> Names.GlobRef.t -> string
val pp_module : Names.ModPath.t -> string
val top_visible_mp : unit -> Names.ModPath.t
val push_visible : Names.ModPath.t -> Names.ModPath.t list -> unit
val pop_visible : unit -> unit
val get_duplicate : Names.ModPath.t -> Names.Label.t -> string option
type reset_kind =
| AllButExternal
| Everything
val reset_renaming_tables : reset_kind -> unit
val set_keywords : Names.Id.Set.t -> unit
val mk_ind : string -> string -> Names.MutInd.t
val is_native_char : Miniml.ml_ast -> bool
val get_native_char : Miniml.ml_ast -> char
val pp_native_char : Miniml.ml_ast -> Pp.t