From 2b799142f66f5f8a55b2c3bb3c954d2858285fee Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 15 Oct 2020 18:57:14 -0700
Subject: Support "Solve Obligations of <ident>" option

---
 plugins/ltac/g_obligations.mlg | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fc24475a62..6bf330c830 100644
--- 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" ] ->
-- 
cgit v1.2.3