chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les options

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

1 files changed, 49 insertions, 0 deletions

diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
new file mode 100644
index 000000000..7efbc0faa
--- /dev/null
+++ b/contrib/extraction/table.mli
@@ -0,0 +1,49 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Summary
+open Goptions
+open Vernacinterp
+open Names
+
+(*s Set and Map over global reference *) 
+
+module Refset : Set.S with type elt = global_reference
+
+(*s Auxiliary functions *) 
+		      
+val check_constant : global_reference -> global_reference
+
+val refs_of_vargl : vernac_arg list -> global_reference list
+
+(*s AutoInline parameter *) 
+
+val auto_inline : unit -> bool
+
+(*s Optimize parameter *) 
+
+val optim :  unit -> bool
+
+(* Table for custom inlining *) 
+
+val to_inline : global_reference -> bool
+
+val to_keep : global_reference -> bool
+
+(*s Table for direct ML extractions. *)
+
+val is_ml_extraction : global_reference -> bool
+
+val find_ml_extraction : global_reference -> string
+
+val ml_extractions : unit -> Refset.t
+
+val sorted_ml_extractions : unit -> (global_reference * string) list
+