1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
9 (*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
14 open OcamlExtractionTable
16 (** By default, in module Format, you can do horizontal placing of blocks
17 even if they include newlines, as long as the number of chars in the
18 blocks are less that a line length. To avoid this awkward situation,
19 we attach a big virtual size to [fnl] newlines. *)
21 val fnl : unit -> std_ppcmds
22 val space_if : bool -> std_ppcmds
24 val pp_par : bool -> std_ppcmds -> std_ppcmds
25 val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
26 val pr_binding : identifier list -> std_ppcmds
28 type env = identifier list * Idset.t
29 val empty_env : #OcamlExtractionTable.status -> env
31 val fake_spec: NReference.spec
33 val rename_tvars: Idset.t -> identifier list -> identifier list
34 val push_vars : identifier list -> env -> identifier list * env
35 val get_db_name : int -> env -> identifier
37 (* true = capitalize *)
38 val modname_of_filename: #status as 'status-> bool -> string -> 'status * string
40 type kind = Term | Type | Cons
43 #status as 'status -> kind -> NReference.reference -> 'status * string