- Fixed many "Theorem with" bugs.

- Fixed doc of assert as.
- Doc of apply in + update credits.
- Nettoyage partiel de Even.v en utilisant "Theorem with".
- Added check that name is not in use for "generalize as".



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

11 files changed, 204 insertions, 175 deletions

diff --git a/CHANGES b/CHANGES
index 326ac272e..72dd72432 100644
--- a/CHANGES
+++ b/CHANGES
@@ -243,6 +243,7 @@ Tactics
   to remember the term to which the induction or case analysis applied
   (possible source of parsing incompatibilities when destruct or induction is
    part of a let-in expression in Ltac; extra parentheses are then required).
+- New support for "as" clause in tactics "apply in" and "eapply in".
 - Some new intro patterns: 
   * intro pattern "?A" genererates a fresh name based on A. 
     Caveat about a slight loss of compatibility:
@@ -285,7 +286,7 @@ Tactics
 - Tactic firstorder "with" and "using" options have their meaning swapped for
   consistency with auto/eauto (source of incompatibility).
 - Tactic "generalize" now supports "at" options to specify occurrences
-  and "as" options to name the hypothesis.
+  and "as" options to name the quantified hypotheses.
 - New tactic "specialize H with a" or "specialize (H a)" allows to transform
   in-place a universally-quantified hypothesis (H : forall x, T x) into its 
   instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index c7f6bf02e..1b6efc582 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -682,8 +682,8 @@ tools.  Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to
 improved the libraries of integers, rational, and real numbers. We
 also thank many users and partners for suggestions and feedback, in
 particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle
-team, the INRIA-Microsoft Mathematical Components team, the
-Foundations group at Radbout university in Nijmegen, reporters of bugs
+team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, 
+the Foundations group at Radbout university in Nijmegen, reporters of bugs
 and participants to the Coq-Club mailing list.
 
 \begin{flushright}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 01ea532e6..ba106e240 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -600,14 +600,31 @@ in the list of subgoals remaining to prove.
   This tactic behaves like \texttt{assert} but applies {\tac}
   to solve the subgoals generated by \texttt{assert}.
 
-\item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
+\item \texttt{assert {\form} as {\intropattern}\tacindex{assert as}}
 
-   This tactic behaves like \texttt{assert ({\ident} : {\form})}.
+  If {\intropattern} is a naming introduction pattern (see
+  Section~\ref{intros-pattern}), the hypothesis is named after this
+  introduction pattern (in particular, if {\intropattern} is {\ident},
+  the tactic behaves like \texttt{assert ({\ident} : {\form})}).
 
-\item \texttt{pose proof {\term} as {\ident}\tacindex{pose proof}}
+  If {\intropattern} is a disjunctive/conjunctive introduction
+  pattern, the tactic behaves like \texttt{assert {\form}} then destructing the
+  resulting hypothesis using the given introduction pattern.
 
-  This tactic behaves like \texttt{assert ({\ident:T}) by exact {\term}} where
-  \texttt{T} is the type of {\term}. 
+\item \texttt{assert {\form} as {\intropattern} by {\tac}}
+
+  This combines the two previous variants of {\tt assert}.
+
+\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
+
+  This tactic behaves like \texttt{assert T as {\intropattern} by
+  exact {\term}} where \texttt{T} is the type of {\term}.
+
+  In particular, \texttt{pose proof {\term} as {\ident}} behaves as
+  \texttt{assert ({\ident}:T) by exact {\term}} (where \texttt{T} is
+  the type of {\term}) and \texttt{pose proof {\term} as
+  {\disjconjintropattern}\tacindex{pose proof}} behaves
+  like \texttt{destruct {\term} as {\disjconjintropattern}}.
 
 \item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)\tacindex{specialize}} \\
       {\tt specialize {\ident} with \bindinglist}
@@ -681,6 +698,17 @@ This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in
 {\ident}} but turns unresolved bindings into existential variables, if
 any, instead of failing.
 
+\item {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in
+{\ident}} then destructs the hypothesis {\ident} along
+{\disjconjintropattern} as {\tt destruct {\ident} as
+{\disjconjintropattern}} would.
+
+\item {\tt eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
+
 \end{Variants}
 
 \subsection{\tt generalize \term
@@ -1779,10 +1807,6 @@ last introduced hypothesis.
   as existential variables to be inferred later, in the same way as
   {\tt eapply} does (see Section~\ref{eapply-example}).
 
-\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
-
-  This tactic behaves like \texttt{destruct {\term} as {\intropattern}}.
-
 \item{\tt destruct {\term$_1$} using {\term$_2$}}\\
      {\tt destruct {\term$_1$} using {\term$_2$} with {\bindinglist}}
 
@@ -1855,6 +1879,9 @@ last introduced hypothesis.
 \subsection{\tt intros {\intropattern} {\ldots} {\intropattern}
 \label{intros-pattern}
 \tacindex{intros \intropattern}}
+\index{Introduction patterns}
+\index{Naming introduction patterns}
+\index{Disjunctive/conjunctive introduction patterns}
 
 This extension of the tactic {\tt intros} combines introduction of
 variables or hypotheses and case analysis. An {\em introduction pattern} is
@@ -4136,7 +4163,7 @@ principles, closer to the definition written by the user.
 
 
 \section{Simple tactic macros
-\index{tactic macros}
+\index{Tactic macros}
 \comindex{Tactic Definition}
 \label{TacticDefinition}}
 
diff --git a/lib/util.ml b/lib/util.ml
index d1e24e321..9428aa134 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -871,6 +871,16 @@ let list_cartesians op init ll =
 
 let list_combinations l = list_cartesians (fun x l -> x::l) [] l
 
+(* Keep only those products that do not return None *)
+
+let rec list_cartesian_filter op l1 l2 = 
+  list_map_append (fun x -> list_map_filter (op x) l2) l1
+
+(* Keep only those products that do not return None *)
+
+let rec list_cartesians_filter op init ll = 
+  List.fold_right (list_cartesian_filter op) ll [init]
+
 (* Drop the last element of a list *)
 
 let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
diff --git a/lib/util.mli b/lib/util.mli
index 46fd7b02e..8b27e6158 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -178,6 +178,11 @@ val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
 val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
+(* Keep only those products that do not return None *)
+val list_cartesian_filter :
+  ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+val list_cartesians_filter :
+  ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
 
 val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0186fcb00..cf603e8fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1250,8 +1250,11 @@ let apply_in with_evars id lemmas ipat gl =
 (*   Generalize tactics   *)
 (**************************)
 
-let generalized_name c t cl = function
-  | Name id as na -> na
+let generalized_name c t ids cl = function
+  | Name id as na ->
+      if List.mem id ids then
+	errorlabstrm "" (pr_id id ++ str " is already used"); 
+      na
   | Anonymous -> 
       match kind_of_term c with
       | Var id ->
@@ -1270,7 +1273,7 @@ let generalize_goal gl i ((occs,c),na) cl =
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in
   let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in
-  let na = generalized_name c t cl' na in
+  let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
   mkProd (na,t,cl')
 
 let generalize_dep c gl =
diff --git a/test-suite/ideal-features/apply.v b/test-suite/ideal-features/apply.v
new file mode 100644
index 000000000..b10d5dbf9
--- /dev/null
+++ b/test-suite/ideal-features/apply.v
@@ -0,0 +1,9 @@
+(* Test propagation of evars from subgoal to brother subgoals *)
+
+(* This does not work (oct 2008) because "match goal" sees "?evar = O" 
+   and not "O = O"
+
+Lemma eapply_evar : O=O -> 0=O.
+intro H; eapply trans_equal; 
+  [apply H | match goal with |- ?x = ?x => reflexivity end].
+Qed.
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
new file mode 100644
index 000000000..4c82d7295
--- /dev/null
+++ b/test-suite/output/set.out
@@ -0,0 +1,21 @@
+1 subgoal
+
+  y1 := 0 : nat
+  x := 0 + 0 : nat
+  ============================
+   x = x
+1 subgoal
+
+  y1 := 0 : nat
+  y2 := 0 : nat
+  x := y2 + 0 : nat
+  ============================
+   x = x
+1 subgoal
+
+  y1 := 0 : nat
+  y2 := 0 : nat
+  y3 := 0 : nat
+  x := y2 + y3 : nat
+  ============================
+   x = x
diff --git a/test-suite/output/set.v b/test-suite/output/set.v
new file mode 100644
index 000000000..0e745354a
--- /dev/null
+++ b/test-suite/output/set.v
@@ -0,0 +1,10 @@
+Goal let x:=O+O in x=x.
+intro.
+set (y1:=O) in (type of x).
+Show.
+set (y2:=O) in (value of x) at 1.
+Show.
+set (y3:=O) in (value of x).
+Show.
+trivial.
+Qed.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index ee3d5fe0d..d2a4006a0 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -52,153 +52,91 @@ Qed.
 
 (** * Facts about [even] & [odd] wrt. [plus] *)
 
-Lemma even_plus_aux :
-  forall n m,
-    (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
-    (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
+Lemma even_plus_split : forall n m, 
+  (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
+with odd_plus_split : forall n m, 
+  odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
 Proof.
-  intros n; elim n; simpl in |- *; auto with arith.
-  intros m; split; auto.
-  split.
-  intros H; right; split; auto with arith.
-  intros H'; case H'; auto with arith.
-  intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
-  intros H; elim H; auto.
-  split; auto with arith.
-  intros H'; elim H'; auto with arith.
-  intros H; elim H; auto.
-  intros H'0; elim H'0; intros H'1 H'2; inversion H'1.
-  intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2;
-    intros E3 E4; clear H'1 H'2.
-  split; split.
-  intros H'0; case E3.
-  inversion H'0; auto.
-  intros H; elim H; intros H0 H1; clear H; auto with arith.
-  intros H; elim H; intros H0 H1; clear H; auto with arith.
-  intros H'0; case H'0; intros C0; case C0; intros C1 C2.
-  apply odd_S.
-  apply E4; left; split; auto with arith.
-  inversion C1; auto.
-  apply odd_S.
-  apply E4; right; split; auto with arith.
-  inversion C1; auto.
-  intros H'0.
-  case E1.
-  inversion H'0; auto.
-  intros H; elim H; intros H0 H1; clear H; auto with arith.
-  intros H; elim H; intros H0 H1; clear H; auto with arith.
-  intros H'0; case H'0; intros C0; case C0; intros C1 C2.
-  apply even_S.
-  apply E2; left; split; auto with arith.
-  inversion C1; auto.
-  apply even_S.
-  apply E2; right; split; auto with arith.
-  inversion C1; auto.
+intros. clear even_plus_split. destruct n; simpl in *.
+ auto with arith.
+ inversion_clear H;
+   apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
+intros. clear odd_plus_split. destruct n; simpl in *.
+ auto with arith.
+ inversion_clear H;
+   apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
 Qed.
- 
-Lemma even_even_plus : forall n m, even n -> even m -> even (n + m).
+
+Lemma even_even_plus : forall n m, even n -> even m -> even (n + m)
+with odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
 Proof.
-  intros n m; case (even_plus_aux n m).
-  intros H H0; case H0; auto.
+intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial.
+intros n m [] ?. apply odd_S, even_even_plus; trivial.
 Qed.
- 
-Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
+
+Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m)
+with odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
 Proof.
-  intros n m; case (even_plus_aux n m).
-  intros H H0; case H0; auto.
+intros n m [|] ?. trivial. apply odd_S, odd_even_plus; trivial.
+intros n m [] ?. apply even_S, odd_plus_r; trivial.
+Qed.
+
+Lemma even_plus_aux : forall n m,
+    (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
+    (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
+Proof.
+split; split; auto using odd_plus_split, even_plus_split.
+intros [[]|[]]; auto using odd_plus_r, odd_plus_l.
+intros [[]|[]]; auto using even_even_plus, odd_even_plus.
 Qed.
 
 Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'0.
-  intros H'1; case H'1; auto.
-  intros H0; elim H0; auto.
-  intros H0 H1 H2; case (not_even_and_odd n); auto.
-  case H0; auto.
+  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd n); auto.
 Qed.
  
 Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'0.
-  intros H'1; case H'1; auto.
-  intros H0; elim H0; auto.
-  intros H0 H1 H2; case (not_even_and_odd m); auto.
-  case H0; auto.
+  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd m); auto.
 Qed.
 
 Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'0.
-  intros H'1; case H'1; auto.
-  intros H0 H1 H2; case (not_even_and_odd n); auto.
-  case H0; auto.
-  intros H0; case H0; auto.
+  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd n); auto.
 Qed.
 
 Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'0.
-  intros H'1; case H'1; auto.
-  intros H0 H1 H2; case (not_even_and_odd m); auto.
-  case H0; auto.
-  intros H0; case H0; auto.
+  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd m); auto.
 Qed.
 Hint Resolve even_even_plus odd_even_plus: arith.
 
-Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
-Proof.
-  intros n m; case (even_plus_aux n m).
-  intros H; case H; auto.
-Qed.
- 
-Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m).
-Proof.
-  intros n m; case (even_plus_aux n m).
-  intros H; case H; auto.
-Qed.
- 
 Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'.
-  intros H'1; case H'1; auto.
-  intros H0 H1 H2; case (not_even_and_odd m); auto.
-  case H0; auto.
-  intros H0; case H0; auto.
+  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd m); auto.
 Qed.
  
 Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'.
-  intros H'1; case H'1; auto.
-  intros H0; case H0; auto.
-  intros H0 H1 H2; case (not_even_and_odd n); auto.
-  case H0; auto.
+  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd n); auto.
 Qed.
  
 Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'.
-  intros H'1; case H'1; auto.
-  intros H0; case H0; auto.
-  intros H0 H1 H2; case (not_even_and_odd m); auto.
-  case H0; auto.
+  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd m); auto.
 Qed.
 
 Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
 Proof.
-  intros n m H; case (even_plus_aux n m).
-  intros H' H'0; elim H'.
-  intros H'1; case H'1; auto.
-  intros H0 H1 H2; case (not_even_and_odd n); auto.
-  case H0; auto.
-  intros H0; case H0; auto.
+  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
+  intro; destruct (not_even_and_odd n); auto.
 Qed.
 Hint Resolve odd_plus_l odd_plus_r: arith.
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4682a963e..050d7ff26 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -346,7 +346,20 @@ let start_proof id kind c ?init_tac hook =
   !start_hook c;
   Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
 
+let adjust_guardness_conditions const =
+  (* Try all combinations... not optimal *)
+  match kind_of_term const.const_entry_body with
+  | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+      let possible_indexes =
+	List.map (fun c ->
+	  interval 0 (List.length (fst (Sign.decompose_lam_assum c))))
+	  (Array.to_list fixdefs) in
+      let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in 
+      { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
+  | c -> const
+
 let save id const (locality,kind) hook =
+  let const = adjust_guardness_conditions const in
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
@@ -1044,13 +1057,12 @@ let build_combined_scheme name schemes =
 (* 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
+  | 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 default_thm_id = id_of_string "Unnamed_thm"
 
@@ -1113,14 +1125,14 @@ let look_for_mutual_statements thms =
         (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) ->
+        List.flatten (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)
+                mind.mind_finite & b = None ->
+              [ind,x,i]
           | _ ->
-              None) 1 whnf_hyp_hds) in
+              []) 1 (List.rev 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
@@ -1128,53 +1140,45 @@ let look_for_mutual_statements thms =
         | Ind (kn,_ as ind) when
               let mind = Global.lookup_mind kn in
               mind.mind_ntypes = n & not mind.mind_finite ->
-            Some (ind,x,0)
+            [ind,x,0]
         | _ ->
-            None in
+            [] 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
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
     (* Check if all conclusions are coinductive in the same type *)
+    (* (degenerated cartesian product since there is at most one coind ccl) *)
     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
+      list_cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks 
+	then Some (hyp::oks) else None) [] ind_ccls in
+    let ordered_same_indccl =
+      List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl 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 *)
+      list_cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks
+	then Some (hyp::oks) else None) [] inds_hyps in
+    let ordered_inds,finite =
+      match ordered_same_indccl, common_same_indhyp with
+      | indccl::rest, _ ->
+	  assert (rest=[]);
+          (* One occ. of common coind ccls and no common inductive hyps *)
+	  if common_same_indhyp <> [] then 
+	    if_verbose warning "Assuming mutual coinductive statements.";
+	  flush_all ();
           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;
+      | [], _::_ ->
+	  if same_indccl <> [] &&
+	     list_distinct (List.map pi1 (List.hd same_indccl)) then
+	    if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+	  (* assume the largest indices as possible *)
+	  list_last common_same_indhyp, false
+      | _, [] ->
+	  error
+            ("Cannot find common (mutual) inductive premises or coinductive" ^
+             " conclusions in the statements.")
+    in
     let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
     let rec_tac =
       if finite then
@@ -1182,6 +1186,7 @@ let look_for_mutual_statements thms =
         | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
         | _ -> assert false
       else
+	(* nl is dummy: it will be recomputed at Qed-time *)
         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