A new command "Separate Extraction"

 This is a mix of "Recursive Extraction" and "Extraction Library":
 - like "Extraction Library", the extracted code is splitted in
   separated files, one per coq source file.
 - unlike "Extraction Library", but similarly to "Recursive Extraction",
   not everything gets extracted, but only dependencies of some
   initially-given elements

 We prepare for a more clever dependency selection inside sub-modules.
 For the moment all needed sub-modules are still fully extracted (other we
 would need to fix signatures accordingly).

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

1 files changed, 11 insertions, 1 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index b9081e286..6d4f06e14 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,13 +175,23 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
 let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
-(*s Extraction mode: modular or monolithic *)
+(*s Extraction modes: modular or monolithic, library or minimal ?
+
+Nota:
+ - Recursive Extraction : monolithic, minimal
+ - Separate Extraction : modular, minimal
+ - Extraction Library : modular, library
+*)
 
 let modular_ref = ref false
+let library_ref = ref false
 
 let set_modular b = modular_ref := b
 let modular () = !modular_ref
 
+let set_library b = library_ref := b
+let library () = !library_ref
+
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].