Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion

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

2 files changed, 46 insertions, 33 deletions

diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 1fe4ee7058..84f0f663b9 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -13,31 +13,23 @@
 open Vernacexpr
 open Pcoq
 open Genarg
+open Pp
 
-let wit_mlname, rawwit_mlname = Genarg.create_arg "mlname"
-let mlname = create_generic_entry "mlname" rawwit_mlname
-let _ = Tacinterp.add_genarg_interp "mlname"
-  (fun ist x ->
-    (in_gen wit_mlname
-      (out_gen wit_string
-	(Tacinterp.genarg_interp ist
-	  (in_gen rawwit_string
-	    (out_gen rawwit_mlname x))))))
-
-GEXTEND Gram
-  GLOBAL: mlname;
-  mlname:
-  [ [ id = IDENT -> id
-    | s = STRING -> s ] ]
-  ;
+VERNAC ARGUMENT EXTEND mlname
+| [ preident(id) ] -> [ id ]
+| [ string(s) ] -> [ s ]
 END
 
-(* Extraction commands *)
-
 open Table
 open Extract_env
-open Pcoq.Constr
-open Pcoq.Prim
+
+VERNAC ARGUMENT EXTEND language
+| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Haskell" ] -> [ Haskell ]
+| [ "Toplevel" ] -> [ Toplevel ]
+END
+
+(* Extraction commands *)
 
 VERNAC COMMAND EXTEND Extraction
 (* Extraction in the Coq toplevel *)
@@ -47,44 +39,58 @@ VERNAC COMMAND EXTEND Extraction
 (* Monolithic extraction to a file *)
 | [ "Extraction" string(f) ne_qualid_list(l) ] 
   -> [ extraction_file f l ]
+END
 
 (* Modular extraction (one Coq module = one ML module) *)
+VERNAC COMMAND EXTEND ExtractionModule
 | [ "Extraction" "Module" ident(m) ]
   -> [ extraction_module m ]
+END
+
+VERNAC COMMAND EXTEND RecursiveExtractionModule
 | [ "Recursive" "Extraction" "Module" ident(m) ]
   -> [ recursive_extraction_module m ]
+END
 
 (* Target Language *)
+VERNAC COMMAND EXTEND ExtractionLanguage
+| [ "Extraction" "Language" language(l) ] 
+  -> [ extraction_language l ]
+END
 
-| [ "Extraction" "Language" "Ocaml" ] 
-  -> [ extraction_language Ocaml ]
-| [ "Extraction" "Language" "Haskell" ] 
-  -> [ extraction_language Haskell ]
-| [ "Extraction" "Language" "Toplevel" ] 
-  -> [ extraction_language Toplevel ]
-
+VERNAC COMMAND EXTEND ExtractionInline
 (* Custom inlining directives *)
 | [ "Extraction" "Inline" ne_qualid_list(l) ] 
   -> [ extraction_inline true l ]
+END
 
+VERNAC COMMAND EXTEND ExtractionNoInline
 | [ "Extraction" "NoInline" ne_qualid_list(l) ] 
   -> [ extraction_inline false l ]
+END
 
+VERNAC COMMAND EXTEND PrintExtractionInline
 | [ "Print" "Extraction" "Inline" ]
   -> [ print_extraction_inline () ]
+END
 
+VERNAC COMMAND EXTEND ResetExtractionInline
 | [ "Reset" "Extraction" "Inline" ]
   -> [ reset_extraction_inline () ]
+END
 
 (* Overriding of a Coq object by an ML one *)
+VERNAC COMMAND EXTEND ExtractionConstant
 | [ "Extract" "Constant" qualid(x) "=>" mlname(y) ]
   -> [ extract_constant_inline false x y ]
+END
 
+VERNAC COMMAND EXTEND ExtractionInlinedConstant
 | [ "Extract" "Inlined" "Constant" qualid(x) "=>" mlname(y) ]
   -> [ extract_constant_inline true x y ]
+END
 
+VERNAC COMMAND EXTEND ExtractionInductive
 | [ "Extract" "Inductive" qualid(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
   -> [ extract_inductive x (id,idl) ]
-
-
 END
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index e1ef0ecc15..92f6f285f8 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -484,10 +484,14 @@ let kill_node_verbose n =
 
 let set_text_mode s = text_proof_flag := s
 
+VERNAC ARGUMENT EXTEND text_mode
+| [ "fr" ] -> [ "fr" ]
+| [ "en" ] -> [ "en" ]
+| [ "Off" ] -> [ "off" ]
+END
+
 VERNAC COMMAND EXTEND TextMode
-| [ "Text" "Mode" "fr" ] -> [ set_text_mode "fr" ]
-| [ "Text" "Mode" "en" ] -> [ set_text_mode "en" ]
-| [ "Text" "Mode" "Off" ] -> [ set_text_mode "off" ]
+| [ "Text" "Mode" text_mode(s) ] -> [ set_text_mode s ]
 END
 
 VERNAC COMMAND EXTEND OutputGoal
@@ -498,8 +502,11 @@ VERNAC COMMAND EXTEND OutputGoal
   [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ]
 END
 
-VERNAC COMMAND EXTEND KillProof
+VERNAC COMMAND EXTEND KillProofAfter
 | [ "Kill" "Proof" "after"  natural(n) ] -> [ kill_node_verbose n ]
+END
+
+VERNAC COMMAND EXTEND KillProofAt
 | [ "Kill" "Proof" "at"  natural(n) ] -> [ kill_node_verbose n ]
 END