Moving the use of Tactic_option from Obligations to G_obligations.

1 files changed, 10 insertions, 4 deletions

diff --git a/tactics/g_obligations.ml4 b/tactics/g_obligations.ml4
index e67d701218..4cd8bf1feb 100644
--- a/tactics/g_obligations.ml4
+++ b/tactics/g_obligations.ml4
@@ -19,16 +19,22 @@ open Constrexpr_ops
 open Stdarg
 open Constrarg
 open Extraargs
-open Pcoq.Prim
-open Pcoq.Constr
-open Pcoq.Tactic
+
+let (set_default_tactic, get_default_tactic, print_default_tactic) = 
+  Tactic_option.declare_tactic_option "Program tactic"
+
+let () =
+  (** Delay to recover the tactic imperatively *)
+  let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
+    snd (get_default_tactic ())
+  end in
+  Obligations.default_tactic := tac
 
 (* We define new entries for programs, with the use of this module
  * Subtac. These entries are named Subtac.<foo>
  *)
 
 module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
 module Tactic = Pcoq.Tactic
 
 open Pcoq