Nettoyage

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

1 files changed, 0 insertions, 27 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ddd5e4220..abacad432 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -368,33 +368,6 @@ ARGUMENT EXTEND hintbases
 | [ ] -> [ Some [] ]
 END
 
-(*
-let wit_hintbases, rawwit_hintbases = Genarg.create_arg "hintbases"
-let hintbases = create_generic_entry "hintbases" rawwit_hintbases
-let _ = Tacinterp.add_interp_genarg "hintbases"
-  (fun ist gl x ->
-    (in_gen wit_hintbases
-      (out_gen (wit_opt (wit_list0 wit_string))
-	(Tacinterp.interp_genarg ist gl
-	  (in_gen (wit_opt (wit_list0 rawwit_string))
-	    (out_gen rawwit_hintbases x))))))
-
-let _ = 
-  Pptactic.declare_extra_genarg_pprule
-    true
-    (rawwit_hintbases, pr_hintbases)
-    (wit_hintbases, pr_hintbases)
-*)
-
-(* V8 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
-
-V8 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*)
 TACTIC EXTEND EAuto
 | [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
     [ gen_eauto false (make_dimension n p) db ]