nouveau design ou le renommage sera fait a posteriori

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

1 files changed, 13 insertions, 18 deletions

diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 485290b03..b42091289 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -5,29 +5,24 @@ open Names
 open Term
 open Miniml
 
-(*s Renaming issues. *)
+(*s Result of an extraction. *)
 
-val get_global_name : identifier -> identifier
+type type_var = Varity | Vskip
 
-type renaming_function = identifier list -> name -> identifier
+type signature = (type_var * identifier) list
 
-module type Renaming = sig
-  val rename_type_parameter : renaming_function
-  val rename_type : renaming_function
-  val rename_term : renaming_function
-  val rename_global_type : renaming_function
-  val rename_global_constructor : renaming_function
-  val rename_global_term : renaming_function
-end
+type extraction_result =
+  | Emltype of ml_type * signature * identifier list
+  | Emlterm of ml_ast
 
-(*s The extraction functor. It returns a single function [extract]
-    translating a piece of CIC environment into a list of ML declarations.
-    The boolean indicates whether cofix are allowed or not. *)
+(*s Extraction functions. *)
 
-module type Translation = sig
-  val extract : bool -> global_reference list -> ml_decl list
-end
+val extract_constr : constr -> extraction_result
 
-module Make : functor (R : Renaming) -> Translation
+val extract_reference : global_reference -> extraction_result
+
+(*s ML declaration corresponding to a Coq reference. *)
+
+val extract_declaration : global_reference -> ml_decl