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

4 files changed, 15 insertions, 35 deletions

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 ->