diff options
| author | Pierre-Marie Pédrot | 2015-12-24 17:55:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-24 18:24:34 +0100 |
| commit | daa7cb065a238c7d4ee394e00315d66d023e5259 (patch) | |
| tree | d50643d775bca154f7ea422786b6d835e48d09fa /tactics/eauto.ml4 | |
| parent | f33fc85b1dd2f4994dc85b0943fe503ace2cc5ff (diff) | |
Removing auto from the tactic AST.
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 33 |
1 files changed, 3 insertions, 30 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ffde67e4fb..1943a4f1f2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -438,37 +438,10 @@ let make_dimension n = function | Some d -> (false,d) open Genarg +open G_auto -(* Hint bases *) - -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - -ARGUMENT EXTEND hintbases - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ "with" "*" ] -> [ None ] -| [ "with" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ Some [] ] -END - -let pr_constr_coma_sequence prc _ _ = - prlist_with_sep pr_comma (fun (_,c) -> prc c) - -ARGUMENT EXTEND constr_coma_sequence - TYPED AS open_constr_list - PRINTED BY pr_constr_coma_sequence -| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ] -| [ open_constr(c) ] -> [ [c] ] -END - -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c) - -ARGUMENT EXTEND auto_using - TYPED AS open_constr_list - PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence(l) ] -> [ l ] -| [ ] -> [ [] ] -END +let hintbases = G_auto.hintbases +let wit_hintbases = G_auto.wit_hintbases TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) |