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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 1 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 4 | ||||
| -rw-r--r-- | plugins/rtauto/proof_search.mli | 2 |
4 files changed, 4 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 13b3dabdf..4d5cbe223 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1415,7 +1415,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto false (false,5) [] (Some []) + Eauto.gen_eauto (false,5) [] (Some []) ] gls @@ -1493,7 +1493,6 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = ( tclCOMPLETE( Eauto.eauto_with_bases - false (true,5) [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7613c6765..8eb7d0e8f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1322,7 +1322,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) e_assumption; Eauto.eauto_with_bases - false (true,5) [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 2448a2d39..d772279f1 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -510,8 +510,8 @@ let pp_gl gl= cut () ++ let pp = function - Incomplete(gl,ctx) -> msgnl (pp_gl gl) - | _ -> msg (str "<complete>") + Incomplete(gl,ctx) -> pp_gl gl ++ fnl () + | _ -> str "<complete>" let pp_info () = let count_info = diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index b236aa721..275e94cde 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,7 +38,7 @@ val branching: state -> state list val success: state -> bool -val pp: state -> unit +val pp: state -> Pp.std_ppcmds val pr_form : form -> unit |