diff options
Diffstat (limited to 'contrib/extraction/common.mli')
-rw-r--r-- | contrib/extraction/common.mli | 50 |
1 files changed, 45 insertions, 5 deletions
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 2ba51e1c..5cd26584 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -6,16 +6,56 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: common.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) open Names +open Libnames open Miniml open Mlutil +open Pp -val print_one_decl : - ml_structure -> module_path -> ml_decl -> unit +val fnl2 : unit -> std_ppcmds +val space_if : bool -> std_ppcmds +val sec_space_if : bool -> std_ppcmds -val print_structure_to_file : - (string * string) option -> extraction_params -> ml_structure -> unit +val pp_par : bool -> std_ppcmds -> std_ppcmds +val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pr_binding : identifier list -> std_ppcmds +val rename_id : identifier -> Idset.t -> identifier +val lowercase_id : identifier -> identifier +val uppercase_id : identifier -> identifier + +val pr_upper_id : identifier -> std_ppcmds + +type env = identifier list * Idset.t +val empty_env : unit -> env + +val rename_vars: Idset.t -> identifier list -> env +val rename_tvars: Idset.t -> identifier list -> identifier list +val push_vars : identifier list -> env -> identifier list * env +val get_db_name : int -> env -> identifier + +val record_contents_fstlev : ml_structure -> unit + +val create_renamings : ml_structure -> module_path list + +type kind = Term | Type | Cons | Mod + +val pp_global : kind -> global_reference -> string +val pp_module : module_path -> string + +val top_visible_mp : unit -> module_path +val push_visible : module_path -> unit +val pop_visible : unit -> unit + +val add_subst : mod_self_id -> module_path -> unit + +val check_duplicate : module_path -> label -> string + +type reset_kind = OnlyLocal | AllButExternal | Everything + +val reset_renaming_tables : reset_kind -> unit + +val set_keywords : Idset.t -> unit |