cleanup table.ml + erreur si Extraction Inline sous section

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

3 files changed, 67 insertions, 65 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 9df2436fa..51ffc6bb4 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -113,29 +113,6 @@ let _ = declare_summary "Extraction tables"
 	    init_function = (fun () -> ());
 	    survive_section = true }
 
-(*S Warning and Error messages. *)
-
-let axiom_scheme_error_message kn = 
-  errorlabstrm "axiom_scheme_message" 
-    (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
-     pr_kn kn ++ spc () ++ str ".") 
-
-let axiom_error_message kn =
-  errorlabstrm "axiom_message"
-    (str "You must specify an extraction for axiom" ++ spc () ++ 
-     pr_kn kn ++ spc () ++ str "first.")
-
-let axiom_warning_message kn = 
-  Options.if_verbose warn 
-    (str "This extraction depends on logical axiom" ++ spc () ++ 
-     pr_kn kn ++ str "." ++ spc() ++ 
-     str "Having false logical axiom in the environment when extracting" ++ 
-     spc () ++ str "may lead to incorrect or non-terminating ML terms.")
-    
-let section_message () = 
-  errorlabstrm "section_message"
-    (str "You can't extract within a section. Close it and try again.")
-
 (*S Generation of flags and signatures. *)
 
 let none = Evd.empty
@@ -234,7 +211,7 @@ let parse_ind_args si args relmax =
 
 let rec extract_type env db j c args = 
   match kind_of_term (whd_betaiotazeta c) with
-    | Var _ -> section_message ()
+    | Var _ -> error_section ()
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -275,8 +252,8 @@ let rec extract_type env db j c args =
 	(* There are two kinds of informative axioms here, *)
 	(* - the types that should be realized via [Extract Constant] *)
 	(* - the type schemes that are not realizable (yet). *) 
-	if args = [] then axiom_error_message kn
-	else axiom_scheme_error_message kn 
+	if args = [] then error_axiom kn
+	else error_axiom_scheme kn 
     | Const kn ->
 	let body = constant_value env kn in 
 	let mlt1 = extract_type env db j (applist (body, args)) [] in 
@@ -528,7 +505,7 @@ let rec extract_term env mle mlt c args =
  	extract_app env mle mlt (extract_fix env mle i recd) args
     | Cast (c, _) -> extract_term env mle mlt c args
     | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false 
-    | Var _ -> section_message ()
+    | Var _ -> error_section ()
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
 
@@ -734,15 +711,11 @@ let extract_constant kn r =
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) -> 
-	       if isSort typ then axiom_error_message kn 
-	       else axiom_scheme_error_message kn
-           | (Info,Default) -> axiom_error_message kn 
-           | (Logic,TypeScheme) ->
-	       axiom_warning_message kn; 
-	       Dtype (r, [], Tdummy)
-	   | (Logic,Default) -> 
-	       axiom_warning_message kn; 
-	       Dterm (r, MLdummy, Tdummy))
+	       if isSort typ then error_axiom kn 
+	       else error_axiom_scheme kn
+           | (Info,Default) -> error_axiom kn 
+           | (Logic,TypeScheme) -> warning_axiom kn; Dtype (r, [], Tdummy)
+	   | (Logic,Default) -> warning_axiom kn; Dterm (r, MLdummy, Tdummy))
     | Some l_body ->
 	(match flag_of_type env typ with
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index af1a9c226..fbc088f20 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -9,19 +9,40 @@
 (*i $Id$ i*)
 
 open Summary
-open Lib
 open Libobject
 open Goptions
-open Vernacinterp
-open Extend
+open Lib
 open Names
+open Libnames
+open Term
+open Declarations
 open Util
 open Pp
-open Term 
-open Declarations
-open Libnames
 open Reduction
 
+(*s Warning and Error messages. *)
+
+let error_axiom_scheme kn = 
+  errorlabstrm "axiom_scheme_message" 
+    (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
+     pr_kn kn ++ spc () ++ str ".") 
+
+let error_axiom kn =
+  errorlabstrm "axiom_message"
+    (str "You must specify an extraction for axiom" ++ spc () ++ 
+     pr_kn kn ++ spc () ++ str "first.")
+
+let warning_axiom kn = 
+  Options.if_verbose warn 
+    (str "This extraction depends on logical axiom" ++ spc () ++ 
+     pr_kn kn ++ str "." ++ spc() ++ 
+     str "Having false logical axiom in the environment when extracting" ++ 
+     spc () ++ str "may lead to incorrect or non-terminating ML terms.")
+    
+let error_section () = 
+  errorlabstrm "section_message"
+    (str "You can't do that within a section. Close it and try again.")
+
 (*s AutoInline parameter *)
 
 let auto_inline_ref = ref true
@@ -125,8 +146,9 @@ let _ = declare_summary "Extraction Inline"
 
 (*s Grammar entries. *)
 
-let extraction_inline b vl =
-  let refs = List.map (fun x -> check_constant (Nametab.global x)) vl in 
+let extraction_inline b l =
+  if sections_are_opened () then error_section (); 
+  let refs = List.map (fun x -> check_constant (Nametab.global x)) l in 
   add_anonymous_leaf (inline_extraction (b,refs))
 
 (*s Printing part *)
@@ -212,25 +234,27 @@ let _ = declare_summary "ML extractions"
 
 (*s Grammar entries. *)
 
-let extract_constant_inline inline qid s =
-  let r,k = check_term_or_type (Nametab.global qid) in
-  add_anonymous_leaf (inline_extraction (inline,[r]));
-  add_anonymous_leaf (in_ml_extraction (r,k,s))
-
-let extract_inductive qid (id2,l2) =
-  let r = Nametab.global qid in match r with
-  | IndRef ((sp,i) as ip) ->
-      let mib = Global.lookup_mind sp in
+let extract_constant_inline inline r s =
+  if sections_are_opened () then error_section (); 
+  let g,k = check_term_or_type (Nametab.global r) in
+  add_anonymous_leaf (inline_extraction (inline,[g]));
+  add_anonymous_leaf (in_ml_extraction (g,k,s))
+
+let extract_inductive r (s,l) =
+  if sections_are_opened () then error_section (); 
+  let g = Nametab.global r in match g with
+  | IndRef ((kn,i) as ip) ->
+      let mib = Global.lookup_mind kn in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
-      if n <> List.length l2 then
+      if n <> List.length l then
 	error "Not the right number of constructors.";
-      add_anonymous_leaf (inline_extraction (true,[r]));
-      add_anonymous_leaf (in_ml_extraction (r,Ind,id2));
+      add_anonymous_leaf (inline_extraction (true,[g]));
+      add_anonymous_leaf (in_ml_extraction (g,Ind,s));
       list_iter_i
 	(fun j s -> 
-	   let r = ConstructRef (ip,succ j) in 
-	   add_anonymous_leaf (inline_extraction (true,[r]));
-	   add_anonymous_leaf (in_ml_extraction (r,Construct,s))) l2
+	   let g = ConstructRef (ip,succ j) in 
+	   add_anonymous_leaf (inline_extraction (true,[g]));
+	   add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l
   | _ -> 
       errorlabstrm "extract_inductive"
-	(Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+	(Printer.pr_global g ++ spc () ++ str "is not an inductive type.")
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index c951116ba..4a21619ac 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -8,10 +8,19 @@
 
 (*i $Id$ i*)
 
-open Vernacinterp
 open Names
 open Libnames
 
+(*s Warning and Error messages. *)
+
+val error_section : unit -> 'a
+
+val error_axiom_scheme : kernel_name -> 'a
+
+val error_axiom : kernel_name -> 'a
+
+val warning_axiom : kernel_name -> unit
+
 (*s AutoInline parameter *) 
 
 val auto_inline : unit -> bool
@@ -49,12 +58,8 @@ val ml_type_extractions : unit -> (global_reference * string) list
 
 val ml_term_extractions : unit -> (global_reference * string) list
 
-
-
 (*s Extraction commands. *)
 
-open Util
-
 val extraction_language : lang -> unit
 
 val extraction_inline : bool -> reference list -> unit