Better handling of aliases, add command to solve a particular obligation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9929 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 05334ad760..d6040646e8 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -104,6 +104,13 @@ VERNAC COMMAND EXTEND Subtac_Obligations
 | [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ]
 END
 
+VERNAC COMMAND EXTEND Subtac_Solve_Obligation
+| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ]
+| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> 
+    [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ]
+      END
+
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
     [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]