Add a generic tactic option builder. Use it in firstorder to set the

default solver (using "Set Firstorder Solver") and for program's
obligation tactic. I don't understand exactly the reason of the warning
when building states/initial.coq, anyone?


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 34 insertions, 40 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c986a3026..f85616279 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -54,7 +54,23 @@ let _=
   in
     declare_int_option gdopt
 
-let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
+let (set_default_solver, default_solver, print_default_solver) = 
+  Tactic_option.declare_tactic_option "Firstorder default solver"
+
+let _ = set_default_solver false (<:tactic<auto with *>>)
+
+VERNAC COMMAND EXTEND Firstorder_Set_Solver
+| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
+    set_default_solver 
+      (Vernacexpr.use_section_locality ())
+      (Tacinterp.glob_tactic t) ]
+END
+
+VERNAC COMMAND EXTEND Firstorder_Print_Solver
+| [ "Print" "Firstorder" "Solver" ] -> [
+    Pp.msgnl
+      (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ]
+END
 
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 
@@ -65,7 +81,7 @@ let gen_ground_tac flag taco ids bases gl=
       let solver=
 	match taco with
 	    Some tac-> tac
-	  | None-> default_solver in
+	  | None-> snd (default_solver ()) in
       let startseq gl=
 	let seq=empty_seq !ground_depth in
 	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
@@ -137,7 +153,7 @@ let default_declarative_automation gls =
     (Cctac.congruence_tac !congruence_depth []))
     (gen_ground_tac true
        (Some (tclTHEN
-		default_solver
+		(snd (default_solver ()))
 		(Cctac.congruence_tac !congruence_depth [])))
        [] []) gls
 
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 113b16800..700e61911 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -161,9 +161,11 @@ VERNAC COMMAND EXTEND Subtac_Set_Solver
       (Tacinterp.glob_tactic t) ]
 END
 
+open Pp
+
 VERNAC COMMAND EXTEND Subtac_Show_Solver
 | [ "Show" "Obligation" "Tactic" ] -> [
-    Pp.msgnl (Pptactic.pr_glob_tactic (Global.env ()) (Subtac_obligations.default_tactic_expr ())) ]
+    msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 5f7114ba5..9619aa422 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -67,10 +67,8 @@ type program_info = {
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
-let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
-let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
-
-let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
+let (set_default_tactic, get_default_tactic, print_default_tactic) = 
+  Tactic_option.declare_tactic_option "Program tactic"
 
 (* true = All transparent, false = Opaque if possible *)
 let proofs_transparency = ref true
@@ -136,10 +134,9 @@ let map_first m =
 
 let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 
-let freeze () = !from_prg, !default_tactic_expr
-let unfreeze (v, t) = from_prg := v; set_default_tactic t
-let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Tacexpr.TacId [])
+let freeze () = !from_prg
+let unfreeze v = from_prg := v
+let init () = from_prg := ProgMap.empty
 
 (** Beware: if this code is dynamically loaded via dynlink after the start
     of Coq, then this [init] function will not be run by [Lib.init ()].
@@ -155,35 +152,16 @@ let _ =
 
 let progmap_union = ProgMap.fold ProgMap.add
 
-let cache (_, (local, tac)) =
-  set_default_tactic tac
-
-let load (_, (local, tac)) =
-  if not local then set_default_tactic tac
-
-let subst (s, (local, tac)) =
-  (local, Tacinterp.subst_tactic s tac)
-
 let (input,output) =
   declare_object
     { (default_object "Program state") with
-      cache_function = cache;
-      load_function = (fun _ -> load);
-      open_function = (fun _ -> load);
-      classify_function = (fun (local, tac) ->
+      classify_function = (fun () ->
 	if not (ProgMap.is_empty !from_prg) then
 	  errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++
 				     prlist_with_sep spc (fun x -> Nameops.pr_id x)
 				     (map_keys !from_prg));
-	if local then Dispose else Substitute (local, tac));
-      subst_function = subst}
+	Dispose) }
     
-let update_state local =
-  Lib.add_anonymous_leaf (input (local, !default_tactic_expr))
-
-let set_default_tactic local t =
-  set_default_tactic t; update_state local
-
 open Evd
 
 let progmap_remove prg =
@@ -469,7 +447,7 @@ let rec solve_obligation prg num tac =
 		  | _ -> ());
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
-	    Pfedit.by !default_tactic;
+	    Pfedit.by (snd (get_default_tactic ()));
 	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac;
 	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
       | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
@@ -501,7 +479,7 @@ and solve_obligation_by_tac prg obls i tac =
 	      | None ->
 		  match obl.obl_tac with
 		  | Some t -> t
-		  | None -> !default_tactic
+		  | None -> snd (get_default_tactic ())
 	    in
 	    let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
 	      obls.(i) <- declare_obligation prg obl t;
@@ -647,6 +625,3 @@ let next_obligation n tac =
     try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
     with Not_found -> anomaly "Could not find a solvable obligation."
   in solve_obligation prg i tac
-
-let default_tactic () = !default_tactic
-let default_tactic_expr () = !default_tactic_expr
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index df7cd684a..c1e8d31c0 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -3,6 +3,7 @@ open Util
 open Libnames
 open Evd
 open Proof_type
+open Vernacexpr
 
 type obligation_info =
   (identifier * Term.types * loc *
@@ -16,8 +17,8 @@ type progress = (* Resolution status of a program *)
   | Defined of global_reference (* Defined as id *)
       
 val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit
-val default_tactic : unit -> Proof_type.tactic
-val default_tactic_expr : unit -> Tacexpr.glob_tactic_expr
+val get_default_tactic : unit -> locality_flag * Proof_type.tactic
+val print_default_tactic : unit -> Pp.std_ppcmds
 
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool