summaryrefslogtreecommitdiff
path: root/contrib/extraction/common.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/extraction/common.mli
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/extraction/common.mli')
-rw-r--r--contrib/extraction/common.mli20
1 files changed, 8 insertions, 12 deletions
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 5cd26584..b7e70414 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.mli 10232 2007-10-17 12:32:10Z letouzey $ i*)
+(*i $Id: common.mli 11559 2008-11-07 22:03:34Z letouzey $ i*)
open Names
open Libnames
@@ -24,11 +24,6 @@ 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
@@ -37,9 +32,12 @@ 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
+type phase = Pre | Impl | Intf
-val create_renamings : ml_structure -> module_path list
+val set_phase : phase -> unit
+val get_phase : unit -> phase
+
+val opened_libraries : unit -> module_path list
type kind = Term | Type | Cons | Mod
@@ -47,14 +45,12 @@ 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 push_visible : module_path -> mod_self_id option -> 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
+type reset_kind = AllButExternal | Everything
val reset_renaming_tables : reset_kind -> unit