diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index c0de6478a4..fb74867f1b 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -176,6 +176,9 @@ let (input,output) = let update_state () = (* msgnl (str "Updating obligations info"); *) Lib.add_anonymous_leaf (input (!from_prg, !default_tactic_expr)) + +let set_default_tactic t = + set_default_tactic t; update_state () open Evd |