diff options
| -rw-r--r-- | tactics/eauto.ml4 | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ddd5e42203..abacad432f 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 ] |