Moving the use of Tactic_option from Obligations to G_obligations.

3 files changed, 15 insertions, 12 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
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 44c83be46c..b2fc456d07 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -323,8 +323,7 @@ let get_info x =
 
 let assumption_message = Declare.assumption_message
 
-let (set_default_tactic, get_default_tactic, print_default_tactic) = 
-  Tactic_option.declare_tactic_option "Program tactic"
+let default_tactic = ref (Proofview.tclUNIT ())
 
 (* true = All transparent, false = Opaque if possible *)
 let proofs_transparency = ref true
@@ -895,7 +894,7 @@ let rec solve_obligation prg num tac =
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
   let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
             Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
-  let _ = Pfedit.by (snd (get_default_tactic ())) in
+  let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
 and obligation (user_num, name, typ) tac =
@@ -924,7 +923,7 @@ and solve_obligation_by_tac prg obls i tac =
 	      | None ->
 		  match obl.obl_tac with
 		  | Some t -> t
-		  | None -> snd (get_default_tactic ())
+		  | None -> !default_tactic
 	    in
 	    let evd = Evd.from_ctx !prg.prg_ctx in
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index e257da0161..3e99f5760b 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -54,10 +54,8 @@ type progress = (* Resolution status of a program *)
   | Remain of int  (* n obligations remaining *)
   | Dependent (* Dependent on other definitions *)
   | Defined of global_reference (* Defined as id *)
-      
-val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val get_default_tactic : unit -> locality_flag * unit Proofview.tactic
-val print_default_tactic : unit -> Pp.std_ppcmds
+
+val default_tactic : unit Proofview.tactic ref
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool