diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-14 12:58:35 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-14 12:58:35 +0000 |
| commit | 8dc08fad7f99f48837e2e617f4d484364f7f8fc3 (patch) | |
| tree | d3ccea189b36edf92504fbac7794a7ea3c65d982 /plugins/subtac/g_subtac.ml4 | |
| parent | 579d0fe3fc304f02100d70d2174807fc5006ab39 (diff) | |
- Show Obligation Tactic
- fix bug #1952.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12668 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/g_subtac.ml4')
| -rw-r--r-- | plugins/subtac/g_subtac.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index fe272edd5..6d4eaabed 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -156,6 +156,11 @@ VERNAC COMMAND EXTEND Subtac_Set_Solver (Tacinterp.glob_tactic t) ] END +VERNAC COMMAND EXTEND Subtac_Show_Solver +| [ "Show" "Obligation" "Tactic" ] -> [ + Pp.msgnl (Pptactic.pr_glob_tactic (Global.env ()) (Subtac_obligations.default_tactic_expr ())) ] +END + VERNAC COMMAND EXTEND Subtac_Show_Obligations | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] |