From b36e75cca2ea910dead09864c4f10ba79b894a35 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 6 Oct 2010 15:48:15 +0000
Subject: Extraction: allow to use Extraction Inline / NoInline even from under
 a section.

 in addition, a makefile entry pluginsopt for compiling only the .cmxs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13509 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/table.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c1b488f350..c22bb17eae 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -482,6 +482,8 @@ let inline_extraction =
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        classify_function = (fun o -> Substitute o);
+       discharge_function =
+	(fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
        subst_function =
         (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -494,7 +496,6 @@ let _ = declare_summary "Extraction Inline"
 (* Grammar entries. *)
 
 let extraction_inline b l =
-  check_inside_section ();
   let refs = List.map Nametab.global l in
   List.iter
     (fun r -> match r with
-- 
cgit v1.2.3