1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
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 11559 2008-11-07 22:03:34Z letouzey $ i*)
17
val fnl2 : unit -> std_ppcmds
18
val space_if : bool -> std_ppcmds
19
val sec_space_if : bool -> std_ppcmds
21
val pp_par : bool -> std_ppcmds -> std_ppcmds
22
val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
23
val pr_binding : identifier list -> std_ppcmds
25
val rename_id : identifier -> Idset.t -> identifier
27
type env = identifier list * Idset.t
28
val empty_env : unit -> env
30
val rename_vars: Idset.t -> identifier list -> env
31
val rename_tvars: Idset.t -> identifier list -> identifier list
32
val push_vars : identifier list -> env -> identifier list * env
33
val get_db_name : int -> env -> identifier
35
type phase = Pre | Impl | Intf
37
val set_phase : phase -> unit
38
val get_phase : unit -> phase
40
val opened_libraries : unit -> module_path list
42
type kind = Term | Type | Cons | Mod
44
val pp_global : kind -> global_reference -> string
45
val pp_module : module_path -> string
47
val top_visible_mp : unit -> module_path
48
val push_visible : module_path -> mod_self_id option -> unit
49
val pop_visible : unit -> unit
51
val check_duplicate : module_path -> label -> string
53
type reset_kind = AllButExternal | Everything
55
val reset_renaming_tables : reset_kind -> unit
57
val set_keywords : Idset.t -> unit