diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 01:22:34 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 01:22:34 +0000 |
| commit | 7da1f2925cd7c355d38f5cfac7d5d3195f6191e9 (patch) | |
| tree | 1b16a7d57c23678e45bd4b400726c836e0c597d8 /contrib/extraction/common.mli | |
| parent | 7c4ffd70946030c74105323f8b45d6d9edfa7ac0 (diff) | |
Extraction des modules, enfin !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/common.mli')
| -rw-r--r-- | contrib/extraction/common.mli | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index fb2291edf..7dae2ae19 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -14,16 +14,10 @@ open Libnames open Miniml open Mlutil -val long_module : global_reference -> dir_path +val print_one_decl : + ml_structure -> module_path -> ml_decl -> unit -val create_mono_renamings : ml_decl list -> unit -val set_keywords : unit -> unit +val print_structure_to_file : + (string * string) option -> extraction_params -> ml_structure -> unit -val pp_decl : unit -> ml_decl -> std_ppcmds -val segment_contents : Lib.library_segment -> global_reference list - -val module_contents : dir_path -> global_reference list - -val extract_to_file : - string option -> extraction_params -> ml_decl list -> unit |