diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-15 10:06:40 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-15 10:06:40 +0000 |
| commit | b31c4c29e921fe581584f051ebc04228303ddfdb (patch) | |
| tree | 88a478593b1685ab5a5d77a7b0c8acaca9524719 /contrib/subtac/g_subtac.ml4 | |
| parent | c33019051c716916414320b8b676202b18e2e8e4 (diff) | |
Various subtac fixes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9485 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 129ac75df..337cc09fc 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -109,6 +109,10 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] END +VERNAC COMMAND EXTEND Subtac_Set_Solver +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ] +END + VERNAC COMMAND EXTEND Subtac_Show_Obligations | [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] | [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] |