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

3 files changed, 37 insertions, 13 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 099bfb3e58..8ab6d23ab5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -380,6 +380,9 @@ let _ =
 TACTIC EXTEND EAuto
 | [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
     [ gen_eauto false (make_dimension n p) db ]
+END
+
+TACTIC EXTEND EAutoDebug
 | [ "EAutod" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
     [ gen_eauto true (make_dimension n p) db ]
 END
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 4a2917c4d7..fd732563a5 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -16,6 +16,17 @@ open Genarg
 
 (* Rewriting orientation *)
 
+let _ = Metasyntax.add_token_obj "<-"
+let _ = Metasyntax.add_token_obj "->"
+
+let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-"
+
+ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
+| [ "->" ] -> [ true ]
+| [ "<-" ] -> [ false ]
+| [ ] -> [ true ]
+END
+(*
 let wit_orient, rawwit_orient = Genarg.create_arg "orient"
 let orient = Pcoq.create_generic_entry "orient" rawwit_orient
 let _ = Tacinterp.add_genarg_interp "orient"
@@ -43,10 +54,30 @@ let _ =
   Pptactic.declare_extra_genarg_pprule
     (rawwit_orient, pr_orient)
     (wit_orient, pr_orient)
-
+*)
  
 (* with_constr *)
 
+open Tacinterp
+
+let pr_with_constr_gen prc = function 
+  | None -> Pp.mt ()
+  | Some c -> Pp.str " with" ++ prc c
+
+let rawpr_with_constr = pr_with_constr_gen Ppconstr.pr_constr
+let pr_with_constr = pr_with_constr_gen Printer.prterm
+
+ARGUMENT EXTEND with_constr
+  TYPED AS constr_opt 
+  PRINTED BY pr_with_constr 
+  INTERPRETED BY genarg_interp
+  RAW TYPED AS constr_opt
+  RAW PRINTED BY rawpr_with_constr
+| [ "with" constr(c) ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+
+(*
 let wit_with_constr, rawwit_with_constr = Genarg.create_arg "with_constr"
 let with_constr = Pcoq.create_generic_entry "with_constr" rawwit_with_constr
 let _ = Tacinterp.add_genarg_interp "with_constr"
@@ -72,16 +103,4 @@ let _ =
   Pptactic.declare_extra_genarg_pprule
     (rawwit_with_constr, pr_with_constr Ppconstr.pr_constr)
     (wit_with_constr, pr_with_constr Printer.prterm)
-
-(*
-(* Clause *)
-let wit_clause, rawwit_clause = Genarg.create_arg "clause"
-let clause = Pcoq.create_generic_entry "clause" rawwit_clause
-let _ = Tacinterp.add_genarg_interp "clause"
-  (fun ist x ->
-    (in_gen wit_clause
-      (out_gen (wit_opt wit_constr)
-	(Tacinterp.genarg_interp ist
-	  (in_gen (wit_opt rawwit_constr)
-	    (out_gen rawwit_clause x))))))
 *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bef676b6ac..8ff06745fd 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -208,7 +208,9 @@ END
 VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s true half_dinv_tac ]
+    END
 
+VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 END