Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

1 files changed, 16 insertions, 1 deletions

diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index a6cde3c5f..9fa7142ce 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -28,7 +28,7 @@ module Refset : Set.S with type elt = global_reference
 		      
 val check_constant : global_reference -> global_reference
 
-val refs_of_vargl : vernac_arg list -> global_reference list
+(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*)
 
 (*s Target language. *)
 
@@ -52,3 +52,18 @@ val ml_extractions : unit -> Refset.t
 
 val sorted_ml_extractions : unit -> (global_reference * string) list
 
+(*s Extraction commands. *)
+
+open Util
+
+val extraction_language : lang -> unit
+
+val extraction_inline : bool -> qualid located list -> unit
+
+val print_extraction_inline : unit -> unit
+
+val reset_extraction_inline : unit -> unit
+
+val extract_constant_inline : bool -> qualid located -> string -> unit
+
+val extract_inductive : qualid located -> string * string list -> unit