diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:57 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-30 09:47:57 +0000 |
commit | 1e1b6828c29b1344f50f94f9d3a6fce27a885656 (patch) | |
tree | e0b7c5a490f8f650262d6a1457b5c64668bd76a2 /tactics/eauto.mli | |
parent | 534cbe4f02392c45567ea30d02b53751482ed767 (diff) |
info_trivial, info_auto, info_eauto, and debug (trivial|auto)
To mitigate the lack of a general "info" tactical, let's
introduce some specialized tactics info_trivial, info_auto
and info_eauto that display the basic tactics used when
solving a goal.
We also add tactics "debug trivial" and "debug auto" which
display every basic tactics attempted by trivial or auto.
Triggering the "info" or "debug" mode for auto, eauto, trivial
can also be done now via global options, such as Set Debug Auto
or Set Info Eauto. In case both debug and info modes are
activated, the debug mode takes precedence.
NB: it would be nice to name these tactics "info xxx" instead
of "info_xxx", but I don't see how to implement a "info eauto"
in eauto.ml4 (hence by TACTIC EXTEND) while keeping
a generic "info foo" tactic in g_ltac.ml4 (useful to display
a nice message about the unavailability of the general info).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.mli')
-rw-r--r-- | tactics/eauto.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 68ec42f4e..5e656139b 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -27,11 +27,11 @@ val registered_e_assumption : tactic val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic -val gen_eauto : bool -> bool * int -> open_constr list -> +val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list -> hint_db_name list option -> tactic val eauto_with_bases : - bool -> + ?debug:Tacexpr.debug -> bool * int -> open_constr list -> Auto.hint_db list -> Proof_type.tactic |