Minor fixes:

- Document and fix [autounfold]
- Fix warning about default Firstorder tactic object not being defined
- Fix treatment of implicits in Program Lemma.


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

3 files changed, 5 insertions, 5 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 3e3e8d177c..d2e45475ef 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -427,7 +427,7 @@ open Extraargs
 
 TACTIC EXTEND autounfold
 | [ "autounfold" hintbases(db) in_arg_hyp(id) ] ->
-    [ autounfold (match db with None -> ["core"] | Some x -> x) 
+    [ autounfold (match db with None -> Auto.current_db_names () | Some [] -> ["core"] | Some x -> x) 
 	(glob_in_arg_hyp_to_clause id) ]
 END
 
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 10e79f733f..d0fa46c7a1 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -10,9 +10,9 @@ open Libobject
 open Proof_type
 open Pp
 
-let declare_tactic_option name =
-  let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC in
-  let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) in
+let declare_tactic_option ?(default=Tacexpr.TacId []) name =
+  let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref default in
+  let default_tactic : Proof_type.tactic ref = ref (Tacinterp.eval_tactic !default_tactic_expr) in
   let locality = ref false in
   let set_default_tactic local t = 
     locality := local;
diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli
index e9cd1f383a..8388738ada 100644
--- a/tactics/tactic_option.mli
+++ b/tactics/tactic_option.mli
@@ -10,7 +10,7 @@ open Proof_type
 open Tacexpr
 open Vernacexpr
 
-val declare_tactic_option : string -> 
+val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> 
   (* put *) (locality_flag -> glob_tactic_expr -> unit) *
   (* get *) (unit -> locality_flag * tactic) *
   (* print *) (unit -> Pp.std_ppcmds)