diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-28 23:50:13 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-28 23:50:13 +0000 |
| commit | a1c371517cba649142559cfe02a8de6a5938893e (patch) | |
| tree | 0fcad89074740343cc74afc177643e17c4933db3 /contrib/extraction/common.mli | |
| parent | 293f86e7c3c4d7bcff03b118369e5e623d3eb6f0 (diff) | |
Remaniement du pp, suite: vers un renommage modulaire correcte
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3336 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/common.mli')
| -rw-r--r-- | contrib/extraction/common.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index d831f00b7..1ae1e1a80 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -16,13 +16,16 @@ open Libnames val long_module : global_reference -> dir_path -val set_globals : unit -> unit +val create_mono_renamings : ml_decl list -> unit +val set_keywords : unit -> unit val pp_logical_ind : global_reference -> std_ppcmds val pp_singleton_ind : global_reference -> std_ppcmds -val pp_decl : bool -> ml_decl -> std_ppcmds +val pp_decl : unit -> ml_decl -> std_ppcmds + +val extract_module : dir_path -> global_reference list val extract_to_file : string option -> extraction_params -> ml_decl list -> unit |