diff options
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 442f18c45..2bd30c5eb 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -355,34 +355,36 @@ open Genarg (* Hint bases *) +let pr_hintbases _prc _prt = function + | None -> str " with *" + | Some [] -> mt () + | Some l -> str " with " ++ Util.prlist str l + +ARGUMENT EXTEND hintbases + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ "with" "*" ] -> [ None ] +| [ "with" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ Some [] ] +END + +(* let wit_hintbases, rawwit_hintbases = Genarg.create_arg "hintbases" let hintbases = create_generic_entry "hintbases" rawwit_hintbases -let _ = Tacinterp.add_genarg_interp "hintbases" +let _ = Tacinterp.add_interp_genarg "hintbases" (fun ist gl x -> (in_gen wit_hintbases (out_gen (wit_opt (wit_list0 wit_string)) - (Tacinterp.genarg_interp ist gl + (Tacinterp.interp_genarg ist gl (in_gen (wit_opt (wit_list0 rawwit_string)) (out_gen rawwit_hintbases x)))))) -GEXTEND Gram - GLOBAL: hintbases; - hintbases: - [ [ "with"; "*" -> None - | "with"; l = LIST1 IDENT -> Some l - | -> Some [] ] ]; -END - -let pr_hintbases = function - | None -> str " with *" - | Some [] -> mt () - | Some l -> str " with " ++ Util.prlist str l - 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) ] -> |