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

1 files changed, 19 insertions, 3 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c986a30260..f85616279d 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