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

10 files changed, 44 insertions, 42 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 07921978d5..5a1014dae5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3207,6 +3207,24 @@ hint.
 
 \SeeAlso Section~\ref{Hints-databases}
 
+\subsection{\tt autounfold with  \ident$_1$ \dots\ \ident$_n$
+\tacindex{autounfold}
+\label{autounfold}}
+
+This tactic unfolds constants that were declared through a {\tt Hint
+  Unfold} in the given databases.
+
+\begin{Variants}
+\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \textit{clause}}
+  
+  Perform the unfolding in the given clause.
+
+\item {\tt autounfold with *}
+  
+  Uses the unfold hints declared in all the hint databases.
+\end{Variants}
+
+
 % EXISTE ENCORE ?
 % 
 % \subsection{\tt Prolog [ \term$_1$ \dots\ \term$_n$ ] \num}
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index acdade7857..c77950c74d 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -53,9 +53,7 @@ let _=
     declare_int_option gdopt
 
 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 *>>)
+  Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
 
 VERNAC COMMAND EXTEND Firstorder_Set_Solver
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index e09008f6ce..8a47dab7c0 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -75,7 +75,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let evm, c, typ, imps =
-    Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr t bl) None
+    Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
     Lemmas.start_proof id kind c (fun loc gr ->
@@ -137,9 +137,6 @@ let subtac (loc, command) =
       Dumpglob.dump_definition lid false "def";
       (match expr with
       | ProveBody (bl, t) ->
-	  if Lib.is_modtype () then
-	    errorlabstrm "Subtac_command.StartProof"
-	      (str "Proof editing mode not supported in module types");
 	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
 	    (fun _ _ -> ())
       | DefineBody (bl, _, c, tycon) ->
@@ -217,33 +214,15 @@ let subtac (loc, command) =
 	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
       in msg_warning cmds
 
-  | Cases.PatternMatchingError (env, exn) as e ->
-      debug 2 (Himsg.explain_pattern_matching_error env exn);
-      raise e
+  | Cases.PatternMatchingError (env, exn) as e -> raise e
 
-  | Type_errors.TypeError (env, exn) as e ->
-      debug 2 (Himsg.explain_type_error env exn);
-      raise e
+  | Type_errors.TypeError (env, exn) as e -> raise e
 
-  | Pretype_errors.PretypeError (env, exn) as e ->
-      debug 2 (Himsg.explain_pretype_error env exn);
-      raise e
+  | Pretype_errors.PretypeError (env, exn) as e -> raise e
 
   | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
-     Loc.Exc_located (loc, e') as e) ->
-      debug 2 (str "Parsing exception: ");
-      (match e' with
-      | Type_errors.TypeError (env, exn) ->
-	  debug 2 (Himsg.explain_type_error env exn);
-	  raise e
-
-      | Pretype_errors.PretypeError (env, exn) ->
-	  debug 2 (Himsg.explain_pretype_error env exn);
-	  raise e
-
-      | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e'');
-	  raise e)
-
-  | e ->
-      msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e);
+     Loc.Exc_located (loc, e') as e) -> raise e
+
+  | e -> 
+      (*       msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e); *)
       raise e
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 3ccb36dc02..2fb1a7981b 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -109,7 +109,7 @@ let env_with_binders env isevars l =
     | [] -> acc
   in aux (env, []) l
 
-let subtac_process env isevars id bl c tycon =
+let subtac_process ?(is_type=false) env isevars id bl c tycon =
   let c = Topconstr.abstract_constr_expr c bl in
   let tycon, imps =
     match tycon with
@@ -122,7 +122,10 @@ let subtac_process env isevars id bl c tycon =
 	    mk_tycon coqt, Some imps
   in
   let c = coqintern_constr !isevars env c in
-  let imps = Option.default (Implicit_quantifiers.implicits_of_rawterm ~with_products:false c) imps in
+  let imps = match imps with 
+    | Some i -> i
+    | None -> Implicit_quantifiers.implicits_of_rawterm ~with_products:is_type c
+  in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars !isevars in
   let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli
index 055c6df22b..48906b23cf 100644
--- a/plugins/subtac/subtac_pretyping.mli
+++ b/plugins/subtac/subtac_pretyping.mli
@@ -16,7 +16,7 @@ val interp :
     Rawterm.rawconstr ->
     Evarutil.type_constraint -> Term.constr * Term.constr
 
-val subtac_process : env -> evar_map ref -> identifier -> local_binder list ->
+val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
 
 val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_map ref -> identifier -> local_binder list ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 618a62f848..dfd92f0c17 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -690,7 +690,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     if resolve_classes then (
       evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
 	~split:true ~fail:fail_evar env !evdref);
-    evdref := consider_remaining_unif_problems env !evdref;
+    evdref := (try consider_remaining_unif_problems env !evdref
+	       with e when not resolve_classes -> 
+		 consider_remaining_unif_problems env 
+		   (Typeclasses.resolve_typeclasses ~onlyargs:false
+		      ~split:true ~fail:fail_evar env !evdref));
     let c = if expand_evar then nf_evar !evdref c' else c' in
       if fail_evar then check_evars env Evd.empty !evdref c;
       c
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)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 4ed3951e5c..49fe20bba2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -74,7 +74,7 @@ Hint Extern 4 => solve_relation : relations.
 
 Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
-Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
+Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R).
 Proof. tauto. Qed.
 
 Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.