Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

13 files changed, 30 insertions, 16 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 93c4504c..d039a930 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: formula.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Hipattern
 open Names
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 558eb876..fbb103c0 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: formula.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Names
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 7451bcd2..19b63407 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma"  i*)
 
-(* $Id$ *)
+(* $Id: g_ground.ml4 13344 2010-07-28 15:04:36Z msozeau $ *)
 
 open Formula
 open Sequent
@@ -54,7 +54,21 @@ 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 ~default:(<:tactic<auto with *>>) "Firstorder default solver"
+
+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 +79,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 +151,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/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 766fa0d3..354bcda2 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: ground.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Formula
 open Sequent
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 3daf66d6..ba8051da 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: ground.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 val ground_tac:     Tacmach.tactic ->
   (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 7da65f08..714604ae 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: instances.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Formula
 open Sequent
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 49716cc6..8b913719 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: instances.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Term
 open Tacmach
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index a35173cd..9cff67dc 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: rules.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 070c1dbe..ec6d2bd0 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: rules.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Tacmach
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 43be5714..1d439693 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: sequent.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Util
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index c310aaff..1232f1e8 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: sequent.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term
 open Util
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 27eca654..835b0409 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: unify.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Formula
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 1412a23e..af2ce01d 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: unify.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Term