diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-24 12:49:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-24 12:49:17 +0000 |
| commit | e870ab98ca09ee2f995fdaaa4e43cd95a9187a18 (patch) | |
| tree | 9bd9a2dfd3bd7395336b2ef1edf05ec8c8de2c25 /contrib/extraction/common.mli | |
| parent | 83c24732cdc8e15fdfa2909825cbdb0fcb9b8352 (diff) | |
suite chgt liés aux modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3029 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/common.mli')
| -rw-r--r-- | contrib/extraction/common.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 9ebb11069..d831f00b7 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -14,9 +14,7 @@ open Mlutil open Names open Libnames -val is_long_module : dir_path -> global_reference -> bool - -val short_module : global_reference -> identifier +val long_module : global_reference -> dir_path val set_globals : unit -> unit @@ -28,5 +26,3 @@ val pp_decl : bool -> ml_decl -> std_ppcmds val extract_to_file : string option -> extraction_params -> ml_decl list -> unit - - |