From 9b50c260c542823589cbca2cec8d57404b5ef419 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 15 Sep 2009 21:32:31 +0000
Subject: Dont't forget to update the state or an obligation tactic assignment
 may have no effect when the module is later imported.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12332 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_obligations.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'plugins')

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
 
-- 
cgit v1.2.3