Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve

des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



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

29 files changed, 474 insertions, 117 deletions

diff --git a/CHANGES b/CHANGES
index 1c3fe7b4c..af156f88b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,7 +1,7 @@
 Changes from V8.1 to V8.2
 =========================
 
-Language 
+Language
 
 - If a fixpoint is not written with an explicit { struct ... }, then 
   all arguments are tried successively (from left to right) until one is 
@@ -16,8 +16,10 @@ Language
   if omitted. (DOC TODO?)
 - Record/Structure now usable for defining coinductive types
   (e.g. "Record stream := { hd : nat; tl : stream }.")
+- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
+  statements.
 
-Commands
+Vernacular commands
 
 - Added option Global to "Arguments Scope" for section surviving. (DOC TODO)
 - Added option "Unset Elimination Schemes" to deactivate the automatic
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 895fa613f..558ca6c21 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1141,7 +1141,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    then
 	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
-	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+	      h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos
 	| _ -> anomaly "Not a valid information"
     in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 31465a7a7..82277be4d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -947,18 +947,22 @@ and xlate_tac =
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
      CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
-    | TacMutualFix (id, n, fixtac_list) ->
+    | TacMutualFix (false, id, n, fixtac_list) ->
      let f (id,n,c) = CT_fixtac (xlate_ident id, CT_int n, xlate_formula c) in
      CT_fixtactic
       (ctf_ID_OPT_SOME (xlate_ident id), CT_int n,
       CT_fix_tac_list (List.map f fixtac_list))
+    | TacMutualFix (true, id, n, fixtac_list) ->
+        xlate_error "TODO: non user-visible fix"
     | TacCofix idopt ->
        CT_cofixtactic (xlate_ident_opt idopt, CT_cofix_tac_list [])
-    | TacMutualCofix (id, cofixtac_list) ->
+    | TacMutualCofix (false, id, cofixtac_list) ->
      let f (id,c) = CT_cofixtac (xlate_ident id, xlate_formula c) in
      CT_cofixtactic
       (CT_coerce_ID_to_ID_OPT (xlate_ident id),
       CT_cofix_tac_list (List.map f cofixtac_list))
+    | TacMutualCofix (true, id, cofixtac_list) ->
+        xlate_error "TODO: non user-visible cofix"
     | TacIntrosUntil (NamedHyp id) -> 
 	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
     | TacIntrosUntil (AnonHyp n) -> 
@@ -1880,10 +1884,12 @@ let rec xlate_vernac =
   | VernacBeginSection (_,id) ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
   | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
-  | VernacStartTheoremProof (k, (_,s), (bl,c), _, _) ->
+  | VernacStartTheoremProof (k, [Some (_,s), (bl,c)], _, _) ->
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,
            xlate_binder_list bl, xlate_formula c))
+  | VernacStartTheoremProof _ ->
+      xlate_error "TODO: Mutually dependent theorems"
   | VernacSuspend -> CT_suspend
   | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt))
   | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) ->
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 1cfe69aa9..9641794be 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -67,10 +67,10 @@ let solve_tccs_in_type env id isevars evm c typ =
 
 let start_proof_com env isevars sopt kind (bl,t) hook =
   let id = match sopt with
-    | Some id ->
+    | Some (loc,id) ->
         (* We check existence here: it's a bit late at Qed time *)
         if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
-          errorlabstrm "start_proof" (pr_id id ++ str " already exists");
+          user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
         id
     | None ->
 	next_global_ident_away false (id_of_string "Unnamed_thm")
@@ -117,13 +117,13 @@ let subtac (loc, command) =
   let isevars = ref (create_evar_defs Evd.empty) in
   try
   match command with
-	VernacDefinition (defkind, (locid, id), expr, hook) -> 
+	VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
 	    (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 id) (Global, DefinitionBody Definition) (bl,t) 
+		  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) 
 		    (fun _ _ -> ())
 	      | DefineBody (bl, _, c, tycon) -> 
 		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
@@ -131,7 +131,7 @@ let subtac (loc, command) =
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
 
-      | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
+      | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
 	  if not(Pfedit.refining ()) then
 	    if lettop then
 	      errorlabstrm "Subtac_command.StartProof"
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 23c19d60b..28cb402f3 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1568,6 +1568,30 @@ All these commands are synonymous of \texttt{Theorem}
 % %within the section will be replaced by the proof of  {\ident}.
 % Same as {\tt Remark} except
 % that the innermost section name is dropped from the full name.
+\item {\tt Theorem \nelist{{\ident} : {\type}}{with}.}
+
+This command is useful for theorems that are proved by simultaneous
+induction over a mutually inductive assumption, or that state mutually
+dependent statements in some mutual coinductive type. It is equivalent
+to {\tt Fixpoint} (see Section~\ref{Fixpoint}) or {\tt CoFixpoint}
+(see Section~\ref{CoFixpoint}) but using tactics to build the proof of
+the statements (or the body of the specification, depending on the
+point of view). The inductive or coinductive types on which the
+induction or coinduction has to be done is assumed to be non ambiguous
+and is guessed by the system. 
+
+Like in a {\tt Fixpoint} or {\tt CoFixpoint} definition, the induction
+hypotheses have to be used on {\em structurally smaller} arguments
+(for a {\tt Fixpoint}) or be {\em guarded by a constructor} (for a {\tt
+  CoFixpoint}).  The verification that recursive proof arguments are
+correct is done only at the time of registering the lemma in the
+environment. To know if the use of induction hypotheses is correct at
+some time of the interactive development of a proof, use the command
+{\tt Guarded} (see Section~\ref{Guarded}).
+
+The command can be used also with {\tt Lemma},
+{\tt Remark}, etc. instead of {\tt Theorem}.
+
 \item {\tt Definition {\ident} : {\type}.} \\
 Allow to define a term of type {\type} using the proof editing mode. It
 behaves as {\tt Theorem} but is intended for the interactive
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1ba08344c..cd32fb35a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -806,6 +806,76 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
+\subsection{\tt fix {\ident} {\num}
+\tacindex{fix}
+\label{tactic:fix}}
+
+This tactic is a primitive tactic to start a proof by induction. In
+general, it is easier to rely on higher-level induction tactics such
+as the ones described in Section~\ref{Tac-induction}.
+
+In the syntax of the tactic, the identifier {\ident} is the name given
+to the induction hypothesis. The natural number {\num} tells on which
+premise of the current goal the induction acts, starting
+from 1 and counting both dependent and non dependent
+products. Especially, the current lemma must be composed of at least
+{\num} products.
+
+Like in a {\tt fix} expression, the induction
+hypotheses have to be used on structurally smaller arguments.
+The verification that inductive proof arguments are correct is done
+only at the time of registering the lemma in the environment. To know
+if the use of induction hypotheses is correct at some
+time of the interactive development of a proof, use the command {\tt
+  Guarded} (see Section~\ref{Guarded}).
+
+\begin{Variants}
+  \item {\tt fix} {\ident}$_1$ {\num} {\tt with (} {\ident}$_2$
+    \nelist{{\binder}$_{2}$}{} \zeroone{{\tt \{ struct {\ident$'_2$}
+      \}}} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt (} {\ident}$_1$
+    \nelist{{\binder}$_n$}{} \zeroone{{\tt \{ struct {\ident$'_n$} \}}}
+           {\tt :} {\type}$_n$ {\tt )}
+
+This starts a proof by mutual induction. The statements to be
+simultaneously proved are respectively {\tt forall}
+  \nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$.  The identifiers
+{\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the induction
+hypotheses. The identifiers {\ident}$'_2$ {\ldots} {\ident}$'_n$ are the
+respective names of the premises on which the induction is performed
+in the statements to be simultaneously proved (if not given, the
+system tries to guess itself what they are).
+
+\end{Variants}
+
+\subsection{\tt cofix {\ident}
+\tacindex{cofix}
+\label{tactic:cofix}}
+
+This tactic starts a proof by coinduction. The identifier {\ident} is
+the name given to the coinduction hypothesis.  Like in a {\tt cofix}
+expression, the use of induction hypotheses have to guarded by a
+constructor.  The verification that the use of coinductive hypotheses
+is correct is done only at the time of registering the lemma in the
+environment. To know if the use of coinduction hypotheses is correct
+at some time of the interactive development of a proof, use the
+command {\tt Guarded} (see Section~\ref{Guarded}).
+
+
+\begin{Variants}
+  \item {\tt cofix} {\ident}$_1$ {\tt with (} {\ident}$_2$
+    \nelist{{\binder}$_2$}{} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt
+      (} {\ident}$_1$ \nelist{{\binder}$_1$}{} {\tt :} {\type}$_n$
+           {\tt )}
+
+This starts a proof by mutual coinduction. The statements to be
+simultaneously proved are respectively {\tt forall}
+\nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$. The identifiers
+    {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the
+    coinduction hypotheses.
+
+\end{Variants}
 
 \section{Negation and contradiction}
 
diff --git a/ide/coq.ml b/ide/coq.ml
index 128717acf..e75f50721 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -351,7 +351,7 @@ let compute_reset_info = function
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
       Reset (id, ref true)
   | VernacDefinition (_, (_,id), ProveBody _, _)
-  | VernacStartTheoremProof (_, (_,id), _, _, _) ->
+  | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
       Reset (id, ref false)
   | _ -> NoReset
 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index c033a6af5..79b4e25aa 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -82,7 +82,7 @@ rule next_order = parse
       { comment_start := lexeme_start lexbuf; comment lexbuf }
   | "Module Type"
       { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
-  | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
+  | "Program" space+ ident { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
   | ident as id 
       { if is_keyword id then 
 	    lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b6a3c985a..035bdced7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -297,14 +297,23 @@ GEXTEND Gram
       | "-" -> false
       | -> true ]]
   ;
+  simple_fix_binder:
+    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
+      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
+    ] ]
+  ;
   fixdecl:
-    [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot;
+    [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ann=fixannot;
         ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
       | -> None ] ]
   ;
+  cofixdecl:
+    [ [ "("; id = ident; bl=LIST0 simple_fix_binder; ":"; ty=lconstr; ")" ->
+        (loc,id,bl,None,ty) ] ]
+  ;
   hintbases:
     [ [ "with"; "*" -> None
       | "with"; l = LIST1 IDENT -> Some l
@@ -387,11 +396,11 @@ GEXTEND Gram
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = ident; n = natural -> TacFix (Some id,n)
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
-	  TacMutualFix (id,n,List.map mk_fix_tac fd)
+	  TacMutualFix (false,id,n,List.map mk_fix_tac fd)
       | "cofix" -> TacCofix None
       | "cofix"; id = ident -> TacCofix (Some id)
-      | "cofix"; id = ident; "with"; fd = LIST1 fixdecl ->
-	  TacMutualCofix (id,List.map mk_cofix_tac fd)
+      | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
+	  TacMutualCofix (false,id,List.map mk_cofix_tac fd)
 
       | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
 	  TacLetTac (Names.Name id,b,nowhere)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index aea0cf27b..8285bbad3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -123,9 +123,11 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders_let; ":";
-        c = lconstr ->
-          VernacStartTheoremProof (thm, id, (bl, c), false, no_hook)
+    [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
+        l = LIST0 
+          [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
+            (Some id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list -> 
 	  VernacAssumption (stre, nl, bl)
       | stre = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2a46388c3..d4befac1e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -687,11 +687,13 @@ and pr_atom1 = function
       hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
   | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
-  | TacMutualFix (id,n,l) ->
+  | TacMutualFix (hidden,id,n,l) ->
+      if hidden then str "idtac" (* should caught before! *) else
       hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_fix_tac l)
   | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
-  | TacMutualCofix (id,l) ->
+  | TacMutualCofix (hidden,id,l) ->
+      if hidden then str "idtac" (* should be caught before! *) else
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc pr_cofix_tac l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9fe24f4d4..57e21c2ce 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -534,12 +534,13 @@ let rec pr_vernac = function
         | None -> mt()
         | Some cc -> str" :=" ++ spc() ++ cc))
 
-  | VernacStartTheoremProof (ki,id,(bl,c),b,d) ->
-      hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++
-      (match bl with
-        | [] -> mt()
-        | _ -> pr_binders bl ++ spc())
-      ++ str":" ++ pr_spc_lconstr c)
+  | VernacStartTheoremProof (ki,l,_,_) ->
+      hov 1 (pr_thm_token ki ++ spc() ++ 
+             prlist_with_sep (fun () -> str "with ") (fun (id,(bl,c)) -> hov 0
+               (pr_opt pr_lident id ++ spc() ++
+                (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+                str":" ++ pr_spc_lconstr c)) l)
+
   | VernacEndProof Admitted -> str"Admitted"
   | VernacEndProof (Proved (opac,o)) -> (match o with
     | None -> if opac then str"Qed" else str"Defined"
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6313a553e..a8ddfadb2 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -313,20 +313,22 @@ let rec mlexpr_of_atomic_tactic = function
       let ido = mlexpr_of_ident_option ido in
       let n = mlexpr_of_int n in
       <:expr< Tacexpr.TacFix $ido$ $n$ >>
-  | Tacexpr.TacMutualFix (id,n,l) ->
+  | Tacexpr.TacMutualFix (b,id,n,l) ->
+      let b = mlexpr_of_bool b in
       let id = mlexpr_of_ident id in
       let n = mlexpr_of_int n in
       let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in
       let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >>
+      <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >>
   | Tacexpr.TacCofix ido ->
       let ido = mlexpr_of_ident_option ido in
       <:expr< Tacexpr.TacCofix $ido$ >>
-  | Tacexpr.TacMutualCofix (id,l) ->
+  | Tacexpr.TacMutualCofix (b,id,l) ->
+      let b = mlexpr_of_bool b in
       let id = mlexpr_of_ident id in
       let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in
       let l = mlexpr_of_list f l in
-      <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
+      <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >>
 
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 91c1bc0c4..11b755fa0 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -34,7 +34,7 @@ let pr_rule = function
   | Nested(cmpd,_) ->
       begin
 	match cmpd with 
-	    Tactic (texp,_) -> hov 0 (pr_tactic texp)
+	  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
 	  | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr)
       end
   | Daimon -> str "<Daimon>"
@@ -50,6 +50,14 @@ let pr_rule_dot = function
   | r ->
       pr_rule r ++ if uses_default_tac r then str "..." else str"."
 
+let pr_rule_dot_fnl = function
+  | Nested (Tactic (TacAtom (_,(TacMutualFix (true,_,_,_)
+                              | TacMutualCofix (true,_,_))),_),_) ->
+      (* Very big hack to not display hidden tactics in "Theorem with" *)
+      (* (would not scale!) *)
+      mt ()
+  | r -> pr_rule_dot r ++ fnl ()
+
 exception Different
 
 (* We remove from the var context of env what is already in osign *)
@@ -155,7 +163,7 @@ let rec print_script nochange sigma pf =
            (print_script nochange sigma) spfl )
     | Some(rule,spfl) ->
 	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
-	   pr_rule_dot rule ++ fnl () ++
+	   pr_rule_dot_fnl rule ++
 	   prlist_with_sep pr_fnl
            (print_script nochange sigma) spfl )	
 
@@ -189,7 +197,7 @@ let print_treescript nochange sigma pf =
     | Some(r,spfl) ->
         let indent = if List.length spfl >= 2 then 1 else 0 in
         (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
-        hv indent (pr_rule_dot r ++ fnl () ++ prlist_with_sep fnl aux spfl)
+        hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl aux spfl)
   in hov 0 (aux pf)
 
 let rec print_info_script sigma osign pf =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d80fdac9d..1701a84c9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -226,10 +226,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	and f2 i =
           if sp1 = sp2 then
             ise_and i
-            [(fun i -> ise_array2 i
-                (fun i -> evar_conv_x env i CONV) al1 al2);
-             (fun i -> ise_list2 i
-                 (fun i -> evar_conv_x env i CONV) l1 l2)]
+            [(fun i -> ise_list2 i 
+                  (fun i -> evar_conv_x env i CONV) l1 l2);
+             (fun i -> solve_refl evar_conv_x env i sp1 al1 al2,
+                  true)]
           else (i,false)
 	in 
 	ise_try evd [f1; f2]
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7df11d332..c5a3cbe3b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -71,6 +71,10 @@ val non_instantiated : evar_map -> (evar * evar_info) list
 (* Unification utils *)
 
 val is_ground_term :  evar_defs -> constr -> bool
+val solve_refl : 
+  (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
+  -> env ->  evar_defs -> existential_key -> constr array -> constr array ->
+    evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
   -> env ->  evar_defs -> conv_pb * existential * constr ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 81216d169..6dad6471d 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,6 +33,7 @@ open Safe_typing
 
 type proof_topstate = {
   mutable top_end_tac : tactic option;
+  top_init_tac : tactic option;
   top_goal : goal;
   top_strength : Decl_kinds.goal_kind;
   top_hook : declaration_hook }
@@ -118,8 +119,6 @@ let delete_proof (loc,id) =
     user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
       
-let init_proofs () = Edit.clear proof_edits
-		       
 let mutate f =
   try 
     Edit.mutate proof_edits (fun _ pfs -> f pfs)
@@ -128,7 +127,8 @@ let mutate f =
       (str"No focused proof" ++ msg_proofs true)
 
 let start (na,ts) =
-  let pfs = mk_pftreestate ts.top_goal in 
+  let pfs = mk_pftreestate ts.top_goal in
+  let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
   add_proof(na,pfs,ts)
     
 let restart_proof () =
@@ -238,7 +238,7 @@ let check_no_pending_proofs () =
 
 let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
 
-let delete_all_proofs = init_proofs
+let delete_all_proofs () = Edit.clear proof_edits
 
 (*********************************************************************)
 (*   Modifying the end tactic of the current profftree               *)
@@ -251,10 +251,11 @@ let set_end_tac tac =
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str sign concl hook =
+let start_proof na str sign concl ?init_tac hook =
   let top_goal = mk_goal sign concl None in
   let ts = { 
     top_end_tac = None;
+    top_init_tac = init_tac;
     top_goal = top_goal;
     top_strength = str;
     top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5de956d46..ad7c5e51a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -71,13 +71,16 @@ val current_proof_depth: unit -> int
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
-(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion
-    [t]; [hook] is optionally a function to be applied at proof end (e.g. to
-    declare the built constructions as a coercion or a setoid morphism) *)
+(*s [start_proof s str env t hook tac] starts a proof of name [s] and
+    conclusion [t]; [hook] is optionally a function to be applied at
+    proof end (e.g. to declare the built constructions as a coercion
+    or a setoid morphism); init_tac is possibly a tactic to
+    systematically apply at initialization time (e.g. to start the
+    proof of mutually dependent theorems) *)
 
 val start_proof : 
-  identifier -> goal_kind -> named_context_val -> constr
-    -> declaration_hook -> unit
+  identifier -> goal_kind -> named_context_val -> constr ->
+    ?init_tac:tactic -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a13f8bf70..34699c5fd 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -26,6 +26,7 @@ type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type split_flag = bool     (* true = exists           false = split *)
+type hidden_flag = bool    (* true = internal use     false = user-level *)
 
 type raw_red_flag =
   | FBeta
@@ -140,9 +141,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCase of evars_flag * 'constr with_bindings
   | TacCaseType of 'constr
   | TacFix of identifier option * int
-  | TacMutualFix of identifier * int * (identifier * int * 'constr) list
+  | TacMutualFix of hidden_flag * identifier * int * (identifier * int * 
+      'constr) list
   | TacCofix of identifier option
-  | TacMutualCofix of identifier * (identifier * 'constr) list
+  | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
   | TacCut of 'constr
   | TacAssert of 'tac option * intro_pattern_expr * 'constr
   | TacGeneralize of 'constr list
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0cb314201..c3b7e0a8b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -49,14 +49,15 @@ let h_elim_type c    = abstract_tactic (TacElimType (inj_open c)) (elim_type c)
 let h_case ev cb     = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb)
 let h_case_type c    = abstract_tactic (TacCaseType (inj_open c)) (case_type c)
 let h_fix ido n      = abstract_tactic (TacFix (ido,n)) (fix ido n)
-let h_mutual_fix id n l =
+let h_mutual_fix b id n l =
   abstract_tactic
-    (TacMutualFix (id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
+    (TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
     (mutual_fix id n l)
+
 let h_cofix ido      = abstract_tactic (TacCofix ido) (cofix ido)
-let h_mutual_cofix id l =
+let h_mutual_cofix b id l =
   abstract_tactic
-    (TacMutualCofix (id,List.map (fun (id,c) -> (id,inj_open c)) l)) 
+    (TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l)) 
     (mutual_cofix id l)
 
 let h_cut c          = abstract_tactic (TacCut (inj_open c)) (cut c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 8cbc28d1e..49415649b 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -43,10 +43,11 @@ val h_elim_type       : constr -> tactic
 val h_case            : evars_flag -> constr with_ebindings -> tactic
 val h_case_type       : constr -> tactic
 
-val h_mutual_fix      : identifier -> int ->
+val h_mutual_fix      : hidden_flag -> identifier -> int ->
                         (identifier * int * constr) list -> tactic
 val h_fix             : identifier option -> int -> tactic
-val h_mutual_cofix    : identifier -> (identifier * constr) list -> tactic
+val h_mutual_cofix    : hidden_flag -> identifier -> 
+                        (identifier * constr) list -> tactic
 val h_cofix           : identifier option -> tactic
 
 val h_cut             : constr -> tactic 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3367f89f1..068ae8e96 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -657,13 +657,13 @@ let rec intern_atomic lf ist x =
   | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
   | TacCaseType c -> TacCaseType (intern_type ist c)
   | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
-  | TacMutualFix (id,n,l) ->
+  | TacMutualFix (b,id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
-      TacMutualFix (intern_ident lf ist id, n, List.map f l)
+      TacMutualFix (b,intern_ident lf ist id, n, List.map f l)
   | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
-  | TacMutualCofix (id,l) ->
+  | TacMutualCofix (b,id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
-      TacMutualCofix (intern_ident lf ist id, List.map f l)
+      TacMutualCofix (b,intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
       TacAssert (Option.map (intern_tactic ist) otac,
@@ -2016,13 +2016,13 @@ and interp_atomic ist gl = function
   | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
   | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n
-  | TacMutualFix (id,n,l) ->
+  | TacMutualFix (b,id,n,l) ->
       let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c)
-      in h_mutual_fix (interp_fresh_ident ist gl id) n (List.map f l)
+      in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l)
   | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt)
-  | TacMutualCofix (id,l) ->
+  | TacMutualCofix (b,id,l) ->
       let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in
-      h_mutual_cofix (interp_fresh_ident ist gl id) (List.map f l)
+      h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l)
   | TacCut c -> h_cut (pf_interp_type ist gl c)
   | TacAssert (t,ipat,c) ->
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
@@ -2350,11 +2350,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb)
   | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
   | TacFix (idopt,n) as x -> x
-  | TacMutualFix (id,n,l) ->
-      TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
+  | TacMutualFix (b,id,n,l) ->
+      TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_rawconstr subst c)) l)
   | TacCofix idopt as x -> x
-  | TacMutualCofix (id,l) ->
-      TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
+  | TacMutualCofix (b,id,l) ->
+      TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
   | TacAssert (b,na,c) ->
       TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c)
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 62c9d3952..cbb387ce9 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,3 +9,17 @@ let fix f (m : nat) : nat := match m with
                              | S m' => f m'
                              end in f 0
      : nat
+fix even_pos_odd_pos 2
+ with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+   omega.
+  
+   apply odd_pos_even_pos in H.
+   omega.
+  
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index fc27e8d28..2b13c2041 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -16,3 +16,26 @@ Check
     end
   in f 0.
 
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0.
+Proof.
+fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+   omega.
+   apply odd_pos_even_pos in H.
+   omega.
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+Show Script.
+Qed.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 108886cf5..78b01f3e1 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -57,3 +57,41 @@ Lemma bx0bx : decomp bx0 = bx1.
 simpl. (* used to return bx0 in V8.1 and before instead of bx1 *)
 reflexivity.
 Qed.
+
+(* Check mutually inductive statements *)
+
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0
+with odd_pos_even_pos : forall n, odd n -> n >= 1.
+Proof.
+ intros.
+ destruct H.
+   omega.
+   apply odd_pos_even_pos in H.
+   omega.
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+Qed.
+
+CoInductive a : Prop := acons : b -> a
+with b : Prop := bcons : a -> b.
+
+Lemma a1 : a
+with b1 : b.
+Proof.
+apply acons.
+assumption.
+
+apply bcons.
+assumption.
+Qed.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d04bbafe3..860a542f4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -136,7 +136,7 @@ let red_constant_entry bl ce = function
 let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
     if local = Local && Flags.is_verbose() then
       msg_warning (pr_id ident ++ str" is declared as a global definition");
     definition_message ident;
@@ -188,7 +188,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
         let kn =
           declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
 	let gr = ConstRef kn in
-	  maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+	  maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
         assumption_message ident;
         if local=Local & Flags.is_verbose () then
           msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -338,28 +338,23 @@ let (inDec,outDec) =
 let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
 
-let start_proof id kind c hook =
+let start_proof id kind c ?init_tac hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
-    !start_hook c;
-    Pfedit.start_proof id kind sign c hook
+  !start_hook c;
+  Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
 
 let save id const (locality,kind) hook =
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
+  let k = logical_kind_of_goal_kind kind in
   let l,r = match locality with
     | Local when Lib.sections_are_opened () ->
-        let k = logical_kind_of_goal_kind kind in
 	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
-    | Local ->
-        let k = logical_kind_of_goal_kind kind in
-        let kn = declare_constant id (DefinitionEntry const, k) in
-	(Global, ConstRef kn)
-    | Global ->
-        let k = logical_kind_of_goal_kind kind in
+    | Local | Global ->
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   Pfedit.delete_current_proof ();
@@ -392,7 +387,7 @@ let make_eq_decidability ind =
     then (message (bl_name^" is already declared."))
     else (
       start_proof (id_of_string bl_name)
-         (Global,Proof Theorem) 
+         (Global,Proof Theorem)
          (Auto_ind_decl.compute_bl_goal ind lnamesparrec nparrec)  
             (fun _ _ -> ());
       Auto_ind_decl.compute_bl_tact ind lnamesparrec nparrec;
@@ -789,7 +784,7 @@ let declare_fix boxed kind f def t imps =
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
-    maybe_declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
     gr
       
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
@@ -1036,24 +1031,171 @@ let build_combined_scheme name schemes =
     if_verbose ppnl (recursive_message Fixpoint None [snd name])
 
 (* 4| Goal declaration *)
-let start_proof_com sopt kind (bl,t) hook =
-  let id = match sopt with
-    | Some id ->
-        (* We check existence here: it's a bit late at Qed time *)
-        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
-          errorlabstrm "start_proof" (pr_id id ++ str " already exists");
-        id
-    | None ->
-	next_global_ident_away false (id_of_string "Unnamed_thm")
- 	  (Pfedit.get_all_proof_names ())
-  in
-  let env = Global.env () in
-  let t = generalize_constr_expr t bl in
-  let it, imps = interp_type_evars_impls env t in
-    start_proof id kind it
-      (fun str cst -> 
-	maybe_declare_manual_implicits false cst (Impargs.is_implicit_args ()) imps;
-	hook str cst)
+
+(* 4.1| Support for mutually proved theorems *)
+
+let retrieve_first_recthm = function
+          | VarRef id -> 
+              (pi2 (Global.lookup_named id),variable_opacity id)
+          | ConstRef cst -> 
+              let {const_body=body;const_opaque=opaq} =
+                Global.lookup_constant cst in
+              (Option.map Declarations.force body,opaq)
+          | _ -> assert false
+
+let compute_proof_name = function
+  | Some (loc,id) ->
+      (* We check existence here: it's a bit late at Qed time *)
+      if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+        user_err_loc (loc,"",pr_id id ++ str " already exists");
+      id
+  | None ->
+      next_global_ident_away false (id_of_string "Unnamed_thm")
+ 	(Pfedit.get_all_proof_names ())
+
+let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
+  match body with
+  | None ->
+      (match local with
+      | Local ->
+          let impl=false and keep=false in (* copy values from Vernacentries *)
+          let k = IsAssumption Conjectural in
+          let c = SectionLocalAssum (t_i,impl,keep) in
+	  let _ = declare_variable id (Lib.cwd(),c,k) in
+          (Local,VarRef id,imps)
+      | Global ->
+          let k = IsAssumption Conjectural in
+          let kn = declare_constant id (ParameterEntry (t_i,false), k) in
+          (Global,ConstRef kn,imps))
+  | Some body ->
+      let k = logical_kind_of_goal_kind kind in
+      let body_i = match kind_of_term body with
+        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+        | CoFix (0,decls) -> mkCoFix (i,decls)
+        | _ -> anomaly "Not a proof by induction" in
+      match local with
+      | Local ->
+	  let c = SectionLocalDef (body_i, Some t_i, opaq) in
+	  let _ = declare_variable id (Lib.cwd(), c, k) in
+          (Local,VarRef id,imps)
+      | Global -> 
+          let const =
+            { const_entry_body = body_i;
+              const_entry_type = Some t_i;
+              const_entry_opaque = opaq;
+              const_entry_boxed = false (* copy of what cook_proof does *)} in
+          let kn = declare_constant id (DefinitionEntry const, k) in
+          (Global,ConstRef kn,imps)
+
+let look_for_mutual_statements thms =
+  if List.tl thms <> [] then
+    (* More than one statement: we look for a common inductive hyp or a *)
+    (* common coinductive conclusion *)
+    let n = List.length thms in
+    let inds = List.map (fun (id,(t,_) as x) -> 
+      let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in
+      let whnf_hyp_hds = map_rel_context_with_binders
+        (fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
+        hyps in
+      let ind_hyps =
+        List.filter ((<>) None) (list_map_i (fun i (_,b,t) ->
+          match kind_of_term t with
+          | Ind (kn,_ as ind) when
+                let mind = Global.lookup_mind kn in
+                mind.mind_ntypes = n & mind.mind_finite & b = None ->
+              Some (ind,x,i)
+          | _ ->
+              None) 1 whnf_hyp_hds) in
+      let ind_ccl =
+        let cclenv = push_rel_context hyps (Global.env()) in
+        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+        match kind_of_term whnf_ccl with
+        | Ind (kn,_ as ind) when
+              let mind = Global.lookup_mind kn in
+              mind.mind_ntypes = n & not mind.mind_finite ->
+            Some (ind,x,0)
+        | _ ->
+            None in
+      ind_hyps,ind_ccl) thms in
+    let inds_hyps,ind_ccls = List.split inds in
+    let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in
+    let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in
+    (* Check if all conclusions are coinductive in the same type *)
+    let same_indccl =
+      match ind_ccls with
+      | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest
+            -> Some (x :: List.map Option.get rest)
+      | _ -> None in
+    (* Check if some hypotheses are inductive in the same type *)
+    let common_same_indhyp =
+      let rec find_same_ind inds = 
+        match inds with
+        | []::_ ->
+            []
+        | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms ->
+            let others' = List.map (List.filter (is_same_ind kn)) other_thms in
+            (x,others')::find_same_ind (hyps_thms1::other_thms)
+        | (None::hyps_thm1)::other_thms ->
+            find_same_ind (hyps_thm1::other_thms)
+      | [] ->
+          assert false in
+      find_same_ind inds_hyps in
+    let common_inds,finite =
+      match same_indccl, common_same_indhyp with
+      | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest ->
+        (* One occurrence of common inductive hyps and no common coind ccls *)
+          Option.get x::List.map (fun x -> Option.get (List.hd x)) rest,
+          false
+      | Some indccl, [] ->
+        (* One occurrence of common coind ccls and no common inductive hyps *)
+          indccl, true
+      | _ -> 
+          error
+            ("Cannot find a common mutual inductive premise or coinductive" ^
+             " conclusion in the statements") in
+    let ordered_inds = List.sort compare_kn common_inds in
+    list_iter_i (fun i' ((kn,i),_,_) -> 
+      if i <> i' then
+        error
+          ("Cannot find distinct (co)inductive types of the same family" ^ 
+              "of mutual (co)inductive types"))
+              ordered_inds;
+    let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
+    let rec_tac =
+      if finite then
+        match List.map (fun (id,(t,_)) -> (id,t)) thms with
+        | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
+        | _ -> assert false
+      else
+        match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+        | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
+        | _ -> assert false in
+    Some rec_tac,thms
+  else
+    None, thms
+
+(* 4.2| General support for goals *)
+
+let start_proof_com kind thms hook =
+  let thms = List.map (fun (sopt,(bl,t)) ->
+    (compute_proof_name sopt,
+     interp_type_evars_impls (Global.env()) (generalize_constr_expr t bl)))
+    thms in
+  let rec_tac,thms = look_for_mutual_statements thms in
+  match thms with
+  | [] -> anomaly "No proof to start"
+  | (id,(t,imps))::other_thms ->
+      let hook strength ref =
+        let other_thms_data =
+          if other_thms = [] then [] else
+            (* there are several theorems defined mutually *)
+            let body,opaq = retrieve_first_recthm ref in
+            list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
+        let thms_data = (strength,ref,imps)::other_thms_data in
+        List.iter (fun (strength,ref,imps) ->
+	  maybe_declare_manual_implicits false ref (is_implicit_args ()) imps;
+	  hook strength ref) thms_data in
+      start_proof id kind t ?init_tac:rec_tac hook
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8a987ef6c..b37c6c359 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -108,10 +108,11 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val set_start_hook : (types -> unit) -> unit
 
 val start_proof : identifier -> goal_kind -> types ->
-  declaration_hook -> unit
+  ?init_tac:Proof_type.tactic -> declaration_hook -> unit
 
-val start_proof_com : identifier option -> goal_kind -> 
-  (local_binder list * constr_expr) -> declaration_hook -> unit
+val start_proof_com : goal_kind -> 
+  (lident option * (local_binder list * constr_expr)) list ->
+  declaration_hook -> unit
 
 (* A hook the next three functions pass to cook_proof *)
 val set_save_hook : (Refiner.pftreestate -> unit) -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 54228e273..473985aed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -295,12 +295,12 @@ let vernac_notation = Metasyntax.add_notation
 (***********)
 (* Gallina *)
 
-let start_proof_and_print idopt k t hook =
-  start_proof_com idopt k t hook;
+let start_proof_and_print k l hook =
+  start_proof_com k l hook;
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
-let vernac_definition (local,_,_ as k) id def hook =
+let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
       if Lib.is_modtype () then
@@ -308,7 +308,8 @@ let vernac_definition (local,_,_ as k) id def hook =
 	  (str "Proof editing mode not supported in module types")
       else
 	let hook _ _ = () in
-	start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook
+	start_proof_and_print (local,DefinitionBody Definition)
+                             [Some lid,(bl,t)] hook
   | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
         | None -> None
@@ -317,7 +318,7 @@ let vernac_definition (local,_,_ as k) id def hook =
 	    Some (interp_redexp env evc r) in
       declare_definition id k bl red_option c typ_opt hook
 
-let vernac_start_proof kind sopt (bl,t) lettop hook =
+let vernac_start_proof kind l lettop hook =
   if not(refining ()) then
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
@@ -325,7 +326,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
   if Lib.is_modtype () then
     errorlabstrm "Vernacentries.StartProof"
       (str "Proof editing mode not supported in module types");
-  start_proof_and_print sopt (Global, Proof kind) (bl,t) hook
+  start_proof_and_print (Global, Proof kind) l hook
 
 let vernac_end_proof = function
   | Admitted -> admit ()
@@ -1051,7 +1052,7 @@ let vernac_goal = function
   | Some c ->
       if not (refining()) then begin
         let unnamed_kind = Lemma (* Arbitrary *) in
-        start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->());
+        start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->());
 	print_subgoals ()
       end else 
 	error "repeated Goal not permitted in refining mode"
@@ -1186,9 +1187,8 @@ let interp c = match c with
   | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
   (* Gallina *)
-  | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
-  | VernacStartTheoremProof (k,(_,id),t,top,f) ->
-      vernac_start_proof k (Some id) t top f
+  | VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f
+  | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f
   | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
@@ -1279,7 +1279,7 @@ let interp c = match c with
   | VernacNop -> ()
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof Theorem None ([],t) false (fun _ _ ->())
+  | VernacGoal t -> vernac_start_proof Theorem [None,([],t)] false (fun _ _->())
   | VernacAbort id -> vernac_abort id
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 976677f8c..7c9998fb4 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -199,8 +199,9 @@ type vernac_expr =
   (* Gallina *)
   | VernacDefinition of definition_kind * lident * definition_expr * 
       declaration_hook
-  | VernacStartTheoremProof of theorem_kind * lident *
-      (local_binder list * constr_expr) * bool * declaration_hook
+  | VernacStartTheoremProof of theorem_kind * 
+      (lident option * (local_binder list * constr_expr)) list *
+        bool * declaration_hook
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list