commandes Extract Constant/Inductive; message d'erreur pour les axiomes

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

1 files changed, 20 insertions, 1 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 1f71ef2f24..a5e7c81af1 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -16,5 +16,24 @@ Grammar vernac vernac : ast :=
 | extr_list   [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
               [ (ExtractionFile $f ($LIST $l)) ]
 | extr_module [ "Extraction" "Module" identarg($m) "." ] ->
-              [ (ExtractionModule $m) ].
+              [ (ExtractionModule $m) ]
 
+| extract_constant 
+     [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
+  -> [ (EXTRACT_CONSTANT $x $y) ]
+
+| extract_inductive 
+     [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
+  -> [ (EXTRACT_INDUCTIVE $x $y) ]
+
+with mindnames : ast :=
+  mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ]
+        -> [(VERNACARGLIST $id ($LIST $idl))]
+
+with idorstring_list: List :=
+  ids_nil  [ ] -> [ ]
+| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ]
+
+with idorstring : ast :=
+  ids_ident  [ identarg($id) ] -> [ $id ]
+| ids_string [ stringarg($s) ] -> [ $s ].