Merge PR #13208: Support "Solve Obligations of <ident>"

Reviewed-by: SkySkimmer
coq · Oct 19, 2020 · 48319ad · 48319ad
2 parents 6ac6f43 + 2b79914
commit 48319ad
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
@@ -111,6 +111,8 @@ END
 VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
 | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
     { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
+| [ "Solve" "Obligations" "of" ident(name) ] ->
+    { try_solve_obligations (Some name) None }
 | [ "Solve" "Obligations" "with" tactic(t) ] ->
     { try_solve_obligations None (Some (Tacinterp.interp t)) }
 | [ "Solve" "Obligations" ] ->