Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ETC etc etc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2141 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 13 deletions

diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 58ee9b662f..2b00192309 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -15,34 +15,39 @@ open Miniml
 open Names
 open Term
 
+val current_module : identifier option ref
+
+val collapse_type_app : ml_type list -> ml_type list
+
 val string : string -> std_ppcmds
 val open_par : bool -> std_ppcmds
 val close_par : bool -> std_ppcmds
+val pp_abst : identifier list -> std_ppcmds
+val pr_binding : identifier list -> std_ppcmds
 
-val collect_lambda : ml_ast -> identifier list * ml_ast
-val push_vars : identifier list -> identifier list * Idset.t ->
-  identifier list * (identifier list * Idset.t)
+val rename_id : identifier -> Idset.t -> identifier
 
-val current_module : identifier option ref
+val lowercase_id : identifier -> identifier
+val uppercase_id : identifier -> identifier
 
-val module_of_r : global_reference -> module_ident
+type env = identifier list * Idset.t
 
-val string_of_r : global_reference -> string
+val rename_vars: Idset.t -> identifier list -> env
+val push_vars : identifier list -> env -> identifier list * env
+val get_db_name : int -> env -> identifier
+val collect_lambda : ml_ast -> identifier list * ml_ast
 
-val check_ml : global_reference -> string -> string
+val keywords : Idset.t
 
-val module_option : global_reference -> string
+val preamble : extraction_params -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
     declarations to a file. *)
 
-open Mlutil
-
 module Make : functor(P : Mlpp_param) -> Mlpp
 
-val current_module : Names.identifier option ref
-val extract_to_file : 
-  string -> extraction_params -> ml_decl list -> unit
+
+