Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).

- tauto/intuition now works uniformly on and, prod, or, sum, False,
  Empty_set, unit, True (and isomorphic copies of them), iff, ->, and
  on all inhabited singleton types with a no-arguments constructor
  such as "eq t t" (even though the last case goes out of
  propositional logic: this features is so often used that it is
  difficult to come back on it).
- New dtauto and dintuition works on all inductive types with one
  constructors and no real arguments (for instance, they work on
  records such as "Equivalence"), in addition to -> and eq-like types.
- Moreover, both of them no longer unfold inner negations (this is a
  souce of incompatibility for intuition and evaluation of the level
  of incompatibility on contribs still needs to be done).

Incidentally, and amazingly, fixing bug #2680 made that constants
InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto
had indeed destructed a section hypothesis "@StrictOrder A ltA@
thinking it was a conjunction, making this section hypothesis
artificially necessary while it was not.

Renouncing to the unfolding of inner negations made auto/eauto
sometimes succeeding more, sometimes succeeding less. There is by the
way a (standard) problem with not in auto/eauto: even when given as an
"unfold hint", it works only in goals, not in hypotheses, so that auto
is not able to solve something like "forall P, (forall x, ~ P x) -> P
0 -> False". Should we automatically add a lemma of type "HYPS -> A ->
False" in the hint database everytime a lemma ""HYPS -> ~A" is
declared (and "unfold not" is a hint), and similarly for all unfold
hints?

At this occasion, also re-did some proofs of Znumtheory.

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

14 files changed, 224 insertions, 141 deletions

diff --git a/CHANGES b/CHANGES
index 91501ebcd..cc365dce9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -41,6 +41,16 @@ Tactics
   "debug trivial" or by a global "Set Debug Auto/Eauto/Trivial".
 - New command "r string" that interprets "idtac string" as a breakpoint
   and jumps to its next use in Ltac debugger.
+- Tactic "tauto" was exceptionally able to destruct other connectives
+  than the binary connectives "and", "or", "prod", "sum", "iff".  This
+  non-uniform behavior has been fixed (bug #2680) and tauto is
+  slightly weaker. On the opposite side, new tactic "dtauto" is able
+  to destruct any record-like inductive types, superseding the old
+  version of "tauto".
+- Similarly, "intuition" has been made more uniform and, where it now
+  fails, "dintuition" can be used. Moreover, both of them are now only
+  lazily unfolding the occurrences of "not" in goal. Some extra
+  "unfold not in *" might have to be added for compatibility.
 
 Libraries
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 6f07eed70..4f1174916 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -81,9 +81,9 @@ let has_nodep_prod = has_nodep_prod_after 0
 
 (* style: None = record; Some false = conjunction; Some true = strict conj *)
 
-let match_with_one_constructor style allow_rec t =
+let match_with_one_constructor style onlybinary allow_rec t =
   let (hdapp,args) = decompose_app t in
-  match kind_of_term hdapp with
+  let res = match kind_of_term hdapp with
   | Ind ind ->
       let (mib,mip) = Global.lookup_inductive ind in
       if (Array.length mip.mind_consnames = 1)
@@ -110,22 +110,25 @@ let match_with_one_constructor style allow_rec t =
 	      None
       else
 	None
+  | _ -> None in
+  match res with
+  | Some (hdapp,args) when not onlybinary || List.length args = 2 -> res
   | _ -> None
 
-let match_with_conjunction ?(strict=false) t =
-  match_with_one_constructor (Some strict) false t
+let match_with_conjunction ?(strict=false) ?(onlybinary=false) t =
+  match_with_one_constructor (Some strict) onlybinary false t
 
 let match_with_record t =
-  match_with_one_constructor None false t
+  match_with_one_constructor None false false t
 
-let is_conjunction ?(strict=false) t =
-  op2bool (match_with_conjunction ~strict t)
+let is_conjunction ?(strict=false) ?(onlybinary=false) t =
+  op2bool (match_with_conjunction ~strict ~onlybinary t)
 
 let is_record t =
   op2bool (match_with_record t)
 
 let match_with_tuple t =
-  let t = match_with_one_constructor None true t in
+  let t = match_with_one_constructor None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd hd in
     let (mib,mip) = Global.lookup_inductive ind in
@@ -146,14 +149,15 @@ let test_strict_disjunction n lc =
     | [_,None,c] -> isRel c && destRel c = (n - i)
     | _ -> false) 0 lc
 
-let match_with_disjunction ?(strict=false) t =
+let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
   let (hdapp,args) = decompose_app t in
-  match kind_of_term hdapp with
+  let res = match kind_of_term hdapp with
   | Ind ind  ->
       let car = mis_constr_nargs ind in
       let (mib,mip) = Global.lookup_inductive ind in
-      if array_for_all (fun ar -> ar = 1) car &&
-	not (mis_is_recursive (ind,mib,mip))
+      if array_for_all (fun ar -> ar = 1) car
+	&& not (mis_is_recursive (ind,mib,mip))
+        && (mip.mind_nrealargs = 0)
       then
 	if strict then
 	  if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
@@ -167,10 +171,13 @@ let match_with_disjunction ?(strict=false) t =
 	  Some (hdapp,Array.to_list cargs)
       else
 	None
+  | _ -> None in
+  match res with
+  | Some (hdapp,args) when not onlybinary || List.length args = 2 -> res
   | _ -> None
 
-let is_disjunction ?(strict=false) t =
-  op2bool (match_with_disjunction ~strict t)
+let is_disjunction ?(strict=false) ?(onlybinary=false) t =
+  op2bool (match_with_disjunction ~strict ~onlybinary t)
 
 (* An empty type is an inductive type, possible with indices, that has no
    constructors *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 82e9e3b8e..e4ae55409 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -53,13 +53,13 @@ val is_non_recursive_type         : testing_function
 
 (** Non recursive type with no indices and exactly one argument for each
    constructor; canonical definition of n-ary disjunction if strict *)
-val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function
-val is_disjunction         : ?strict:bool -> testing_function
+val match_with_disjunction : ?strict:bool -> ?onlybinary:bool -> (constr * constr list) matching_function
+val is_disjunction         : ?strict:bool -> ?onlybinary:bool -> testing_function
 
 (** Non recursive tuple (one constructor and no indices) with no inner
    dependencies; canonical definition of n-ary conjunction if strict *)
-val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
-val is_conjunction         : ?strict:bool -> testing_function
+val match_with_conjunction : ?strict:bool -> ?onlybinary:bool -> (constr * constr list) matching_function
+val is_conjunction         : ?strict:bool -> ?onlybinary:bool -> testing_function
 
 (** Non recursive tuple, possibly with inner dependencies *)
 val match_with_record      : (constr * constr list) matching_function
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 036c4f0ea..12bb36eb4 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -28,22 +28,30 @@ let assoc_var s ist =
 
 (** Parametrization of tauto *)
 
+type tauto_flags = {
+
 (* Whether conjunction and disjunction are restricted to binary connectives *)
-(* (this is the compatibility mode) *)
-let binary_mode = true
+  binary_mode : bool;
+
+(* Whether compatibility for buggy detection of binary connective is on *)
+  binary_mode_bugged_detection : bool;
 
 (* Whether conjunction and disjunction are restricted to the connectives *)
 (* having the structure of "and" and "or" (up to the choice of sorts) in *)
-(* contravariant position in an hypothesis (this is the compatibility mode) *)
-let strict_in_contravariant_hyp = true
+(* contravariant position in an hypothesis *)
+  strict_in_contravariant_hyp : bool;
 
 (* Whether conjunction and disjunction are restricted to the connectives *)
 (* having the structure of "and" and "or" (up to the choice of sorts) in *)
 (* an hypothesis and in the conclusion *)
-let strict_in_hyp_and_ccl = false
+  strict_in_hyp_and_ccl : bool;
 
 (* Whether unit type includes equality types *)
-let strict_unit = false
+  strict_unit : bool;
+
+(* Whether inner unfolding is allowed *)
+  inner_unfolding : bool
+}
 
 (* Whether inner iff are unfolded *)
 let iff_unfolding = ref false
@@ -70,8 +78,8 @@ let is_empty ist =
 
 (* Strictly speaking, this exceeds the propositional fragment as it
    matches also equality types (and solves them if a reflexivity) *)
-let is_unit_or_eq ist =
-  let test = if strict_unit then is_unit_type else is_unit_or_eq_type in
+let is_unit_or_eq flags ist =
+  let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
   if test (assoc_var "X1" ist) then
     <:tactic<idtac>>
   else
@@ -85,13 +93,13 @@ let is_record t =
 	    mib.Declarations.mind_record
       | _ -> false
 
-let is_binary t =
+let bugged_is_binary t =
   isApp t &&
   let (hdapp,args) = decompose_app t in
     match (kind_of_term hdapp) with
     | Ind ind  ->
         let (mib,mip) = Global.lookup_inductive ind in
-	  mib.Declarations.mind_nparams = 2
+         mib.Declarations.mind_nparams = 2
     | _ -> false
 
 let iter_tac tacl =
@@ -99,70 +107,72 @@ let iter_tac tacl =
 
 (** Dealing with conjunction *)
 
-let is_conj ist =
+let is_conj flags ist =
   let ind = assoc_var "X1" ist in
-    if (not binary_mode || is_binary ind) (* && not (is_record ind) *)
-      && is_conjunction ~strict:strict_in_hyp_and_ccl ind
+    if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) &&
+       is_conjunction
+         ~strict:flags.strict_in_hyp_and_ccl
+         ~onlybinary:flags.binary_mode ind
     then
       <:tactic<idtac>>
     else
       <:tactic<fail>>
 
-let flatten_contravariant_conj ist =
+let flatten_contravariant_conj flags ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
+  match match_with_conjunction
+          ~strict:flags.strict_in_contravariant_hyp
+          ~onlybinary:flags.binary_mode typ
+  with
   | Some (_,args) ->
-      let i = List.length args in
-      if not binary_mode || i = 2 then
-	let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in
-	let hyp = valueIn (VConstr ([],hyp)) in
-	let intros =
-	  iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
-	  <:tactic< idtac >> in
-	<:tactic<
-          let newtyp := $newtyp in
-          let hyp := $hyp in
-	  assert newtyp by ($intros; apply hyp; split; assumption);
-	  clear hyp
-	>>
-      else
-	<:tactic<fail>>
+      let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in
+      let hyp = valueIn (VConstr ([],hyp)) in
+      let intros =
+	iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
+	<:tactic< idtac >> in
+      <:tactic<
+        let newtyp := $newtyp in
+        let hyp := $hyp in
+	assert newtyp by ($intros; apply hyp; split; assumption);
+	clear hyp
+      >>
   | _ ->
       <:tactic<fail>>
 
 (** Dealing with disjunction *)
 
-let is_disj ist =
+let is_disj flags ist =
   let t = assoc_var "X1" ist in
-  if (not binary_mode || is_binary t) &&
-    is_disjunction ~strict:strict_in_hyp_and_ccl t
+  if (not flags.binary_mode_bugged_detection || bugged_is_binary t) &&
+     is_disjunction
+       ~strict:flags.strict_in_hyp_and_ccl
+       ~onlybinary:flags.binary_mode t
   then
     <:tactic<idtac>>
   else
     <:tactic<fail>>
 
-let flatten_contravariant_disj ist =
+let flatten_contravariant_disj flags ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
+  match match_with_disjunction
+          ~strict:flags.strict_in_contravariant_hyp
+          ~onlybinary:flags.binary_mode
+          typ with
   | Some (_,args) ->
-      let i = List.length args in
-      if not binary_mode || i = 2 then
-	let hyp = valueIn (VConstr ([],hyp)) in
-	iter_tac (list_map_i (fun i arg ->
-	  let typ = valueIn (VConstr ([],mkArrow arg c)) in
-	  let i = Tacexpr.Integer i in
-	  <:tactic<
-            let typ := $typ in
-            let hyp := $hyp in
-	    let i := $i in
-	    assert typ by (intro; apply hyp; constructor i; assumption)
-	  >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
-      else
-	<:tactic<fail>>
+      let hyp = valueIn (VConstr ([],hyp)) in
+      iter_tac (list_map_i (fun i arg ->
+	let typ = valueIn (VConstr ([],mkArrow arg c)) in
+	let i = Tacexpr.Integer i in
+	<:tactic<
+          let typ := $typ in
+          let hyp := $hyp in
+	  let i := $i in
+	  assert typ by (intro; apply hyp; constructor i; assumption)
+	>>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
   | _ ->
       <:tactic<fail>>
 
@@ -173,13 +183,11 @@ let not_dep_intros ist =
   <:tactic<
   repeat match goal with
   | |- (forall (_: ?X1), ?X2) => intro
-  | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not at 1
-  | H:(Coq.Init.Logic.not _)|-_    => unfold Coq.Init.Logic.not at 1 in H
-  | H:forall (_: Coq.Init.Logic.not _), _|-_    => unfold Coq.Init.Logic.not at 1 in H
+  | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
   end >>
 
-let axioms ist =
-  let t_is_unit_or_eq = tacticIn is_unit_or_eq
+let axioms flags ist =
+  let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags)
   and t_is_empty = tacticIn is_empty in
     <:tactic<
     match reverse goal with
@@ -189,12 +197,12 @@ let axioms ist =
     end >>
 
 
-let simplif ist =
-  let t_is_unit_or_eq = tacticIn is_unit_or_eq
-  and t_is_conj = tacticIn is_conj
-  and t_flatten_contravariant_conj = tacticIn flatten_contravariant_conj
-  and t_flatten_contravariant_disj = tacticIn flatten_contravariant_disj
-  and t_is_disj = tacticIn is_disj
+let simplif flags ist =
+  let t_is_unit_or_eq = tacticIn (is_unit_or_eq flags)
+  and t_is_conj = tacticIn (is_conj flags)
+  and t_flatten_contravariant_conj = tacticIn (flatten_contravariant_conj flags)
+  and t_flatten_contravariant_disj = tacticIn (flatten_contravariant_disj flags)
+  and t_is_disj = tacticIn (is_disj flags)
   and t_not_dep_intros = tacticIn not_dep_intros in
   <:tactic<
     $t_not_dep_intros;
@@ -231,11 +239,11 @@ let simplif ist =
         end;
         $t_not_dep_intros) >>
 
-let rec tauto_intuit t_reduce solver ist =
-  let t_axioms = tacticIn axioms
-  and t_simplif = tacticIn simplif
-  and t_is_disj = tacticIn is_disj
-  and t_tauto_intuit = tacticIn (tauto_intuit t_reduce solver) in
+let rec tauto_intuit flags t_reduce solver ist =
+  let t_axioms = tacticIn (axioms flags)
+  and t_simplif = tacticIn (simplif flags)
+  and t_is_disj = tacticIn (is_disj flags)
+  and t_tauto_intuit = tacticIn (tauto_intuit flags t_reduce solver) in
   let t_solver = globTacticIn (fun _ist -> solver) in
   <:tactic<
    ($t_simplif;$t_axioms
@@ -247,6 +255,10 @@ let rec tauto_intuit t_reduce solver ist =
 		[ exact id
 		| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
 		  solve [ $t_tauto_intuit ]]]
+      | id:forall (_:not ?X1), ?X3|- _ =>
+	  cut X3;
+	    [ intro; clear id; $t_tauto_intuit
+	    | cut (not X1); [ exact id | clear id; intro; solve [$t_tauto_intuit ]]]
       | |- ?X1 =>
           $t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit]
       end
@@ -267,11 +279,13 @@ let reduction_not _ist =
 
 let t_reduction_not = tacticIn reduction_not
 
-let intuition_gen tac =
-  interp (tacticIn (tauto_intuit t_reduction_not tac))
+let intuition_gen flags tac =
+  let t_reduce =
+    if flags.inner_unfolding then t_reduction_not else  <:tactic<idtac>> in
+  interp (tacticIn (tauto_intuit flags t_reduce tac))
 
-let tauto_intuitionistic g =
-  try intuition_gen <:tactic<fail>> g
+let tauto_intuitionistic flags g =
+  try intuition_gen flags <:tactic<fail>> g
   with
     Refiner.FailError _ | UserError _ ->
       errorlabstrm "tauto" (str "tauto failed.")
@@ -280,26 +294,69 @@ let coq_nnpp_path =
   let dir = List.map id_of_string ["Classical_Prop";"Logic";"Coq"] in
   Libnames.make_path (make_dirpath dir) (id_of_string "NNPP")
 
-let tauto_classical nnpp g =
-  try tclTHEN (apply nnpp) tauto_intuitionistic g
+let tauto_classical flags nnpp g =
+  try tclTHEN (apply nnpp) (tauto_intuitionistic flags) g
   with UserError _ -> errorlabstrm "tauto" (str "Classical tauto failed.")
 
-let tauto g =
+let tauto_gen flags g =
   try
     let nnpp = constr_of_global (Nametab.global_of_path coq_nnpp_path) in
     (* try intuitionistic version first to avoid an axiom if possible *)
-    tclORELSE tauto_intuitionistic (tauto_classical nnpp) g
+    tclORELSE (tauto_intuitionistic flags) (tauto_classical flags nnpp) g
   with Not_found ->
-    tauto_intuitionistic g
-
+    tauto_intuitionistic flags g
 
 let default_intuition_tac = <:tactic< auto with * >>
 
+(* This is the uniform mode dealing with ->, not, iff and types isomorphic to
+   /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types;
+   not and iff are unfolded only if necessary *)
+let tauto_uniform_unit_flags = {
+  binary_mode = true;
+  binary_mode_bugged_detection = false;
+  strict_in_contravariant_hyp = true;
+  strict_in_hyp_and_ccl = true;
+  strict_unit = false;
+  inner_unfolding = false
+}
+
+(* This is the compatibility mode (not used) *)
+let tauto_legacy_flags = {
+  binary_mode = true;
+  binary_mode_bugged_detection = true;
+  strict_in_contravariant_hyp = true;
+  strict_in_hyp_and_ccl = false;
+  strict_unit = false;
+  inner_unfolding = true
+}
+
+(* This is the improved mode *)
+let tauto_power_flags = {
+  binary_mode = false; (* support n-ary connectives *)
+  binary_mode_bugged_detection = false;
+  strict_in_contravariant_hyp = false; (* supports non-regular connectives *)
+  strict_in_hyp_and_ccl = false;
+  strict_unit = false;
+  inner_unfolding = false
+}
+
+let tauto = tauto_gen tauto_uniform_unit_flags
+let dtauto = tauto_gen tauto_power_flags
+
 TACTIC EXTEND tauto
 | [ "tauto" ] -> [ tauto ]
 END
 
+TACTIC EXTEND dtauto
+| [ "dtauto" ] -> [ dtauto ]
+END
+
 TACTIC EXTEND intuition
-| [ "intuition" ] -> [ intuition_gen default_intuition_tac ]
-| [ "intuition" tactic(t) ] -> [ intuition_gen t ]
+| [ "intuition" ] -> [ intuition_gen tauto_uniform_unit_flags default_intuition_tac ]
+| [ "intuition" tactic(t) ] -> [ intuition_gen tauto_uniform_unit_flags t ]
+END
+
+TACTIC EXTEND dintuition
+| [ "dintuition" ] -> [ intuition_gen tauto_power_flags default_intuition_tac ]
+| [ "dintuition" tactic(t) ] -> [ intuition_gen tauto_power_flags t ]
 END
diff --git a/test-suite/bugs/closed/shouldsucceed/2680.v b/test-suite/bugs/closed/shouldsucceed/2680.v
new file mode 100644
index 000000000..0f573a289
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2680.v
@@ -0,0 +1,17 @@
+(* Tauto bug initially due to wrong test for binary connective *)
+
+Parameter A B : Type.
+
+Axiom P : A -> B ->  Prop.
+
+Inductive IP (a  : A) (b: B) : Prop :=
+| IP_def : P a b ->   IP a b.
+
+
+Goal forall (a : A) (b : B), IP a b ->  ~ IP a b -> False.
+Proof.
+  intros.
+  tauto.
+Qed.
+
+
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 9f44d4fef..87f86e0d3 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -139,7 +139,7 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
       | _, _ => in_right
     end }.
 
-  Next Obligation. destruct y ; intuition eauto. Defined.
+  Next Obligation. destruct y ; unfold not in *; eauto. Defined.
 
   Solve Obligations with unfold equiv, complement in * ; 
     program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index a8de1ba08..3717e1cb4 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -130,7 +130,7 @@ Tactic Notation "apply" "*" constr(t) :=
 
 Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
-    try ( solve [ intuition ]).
+    try ( solve [ dintuition ]).
 
 Local Obligation Tactic := simpl_relation.
 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 0c1448c9b..9fef1dc63 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -519,7 +519,7 @@ Proof.
 intros. rewrite eq_option_alt. intro e.
 rewrite <- find_mapsto_iff, elements_mapsto_iff.
 unfold eqb.
-rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto.
+rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto.
 Qed.
 
 Lemma elements_b : forall m x,
@@ -679,8 +679,8 @@ Add Parametric Morphism elt : (@Empty elt)
  with signature Equal ==> iff as Empty_m.
 Proof.
 unfold Empty; intros m m' Hm; intuition.
-rewrite <-Hm in H0; eauto.
-rewrite Hm in H0; eauto.
+rewrite <-Hm in H0; eapply H, H0.
+rewrite Hm in H0; eapply H, H0.
 Qed.
 
 Add Parametric Morphism elt : (@is_empty elt)
@@ -1872,13 +1872,7 @@ Module OrdProperties (M:S).
     add_mapsto_iff by (auto with *).
   unfold O.eqke, O.ltk; simpl.
   destruct (E.compare t0 x); intuition.
-  right; split; auto; ME.order.
-  ME.order.
-  elim H.
-  exists e0; apply MapsTo_1 with t0; auto.
-  right; right; split; auto; ME.order.
-  ME.order.
-  right; split; auto; ME.order.
+  elim H; exists e0; apply MapsTo_1 with t0; auto.
   Qed.
 
   Lemma elements_Add_Above : forall m m' x e,
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 1bad80615..eec7196b7 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -995,8 +995,6 @@ Module OrdProperties (M:S).
    leb_1, gtb_1, (H0 a) by auto with *.
   intuition.
   destruct (E.compare a x); intuition.
-  right; right; split; auto with *.
-  ME.order.
   Qed.
 
   Definition Above x s := forall y, In y s -> E.lt y x.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 70f4ff0d9..944e7da21 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -43,7 +43,7 @@ Hint Immediate Rge_refl: rorders.
 
 Lemma Rlt_irrefl : forall r, ~ r < r.
 Proof.
-  generalize Rlt_asym. intuition eauto.
+  intros r H; eapply Rlt_asym; eauto.
 Qed.
 Hint Resolve Rlt_irrefl: real.
 
@@ -64,7 +64,9 @@ Qed.
 (**********)
 Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2.
 Proof.
-  generalize Rlt_not_eq Rgt_not_eq. intuition eauto.
+  intuition.
+  - apply Rlt_not_eq in H1. eauto.
+  - apply Rgt_not_eq in H1. eauto.
 Qed.
 Hint Resolve Rlt_dichotomy_converse: real.
 
@@ -74,7 +76,7 @@ Hint Resolve Rlt_dichotomy_converse: real.
 Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
 Proof.
   intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
-    intuition eauto 3.
+    unfold not; intuition eauto 3.
 Qed.
 Hint Resolve Req_dec: real.
 
@@ -175,7 +177,7 @@ Proof. eauto using Rnot_gt_ge with rorders. Qed.
 Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
 Proof.
   generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
-  intuition eauto 3.
+  unfold not; intuition eauto 3.
 Qed.
 Hint Immediate Rlt_not_le: real.
 
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index 0a8d89c77..eeafbde9b 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -15,7 +15,7 @@ Local Open Scope R_scope.
 Lemma Req_dec : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
 Proof.
   intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
-    intuition eauto 3.
+    intuition eauto.
 Qed.
 
 Definition Reqb r1 r2 := if Req_dec r1 r2 then true else false.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index f84cdf32c..beb10a833 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -223,7 +223,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
 Proof. exact (InfA_ltA lt_strorder). Qed.
 
 Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
 
 Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
 Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
@@ -396,7 +396,7 @@ Module KeyOrderedType(O:OrderedType).
   Qed.
 
   Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed.
+  Proof. exact (InfA_eqA eqk_equiv ltk_compat). Qed.
 
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index f83b63779..059992f5b 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -32,7 +32,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
 Proof. exact (InfA_ltA lt_strorder). Qed.
 
 Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
 
 Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
 Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 6eb1a7093..2d4bfb2e3 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -575,30 +575,29 @@ Lemma prime_divisors :
   forall p:Z,
     prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
 Proof.
-  simple induction 1; intros.
+  destruct 1; intros.
   assert
     (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).
-  assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ].
-  generalize H3.
-  pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *;
-    apply Zabs_ind; intros; omega.
+  { assert (Zabs a <= Zabs p) as H2.
+      apply Zdivide_bounds; [ assumption | omega ].
+    revert H2.
+    pattern (Zabs a); apply Zabs_ind; pattern (Zabs p); apply Zabs_ind;
+    intros; omega. }
   intuition idtac.
   (* -p < a < -1 *)
-  absurd (rel_prime (- a) p); intuition.
-  inversion H3.
-  assert (- a | - a); auto with zarith.
-  assert (- a | p); auto with zarith.
-  generalize (H8 (- a) H9 H10); intuition idtac.
-  generalize (Zdivide_1 (- a) H11); intuition.
+  - absurd (rel_prime (- a) p); intuition.
+    inversion H2.
+    assert (- a | - a) by auto with zarith.
+    assert (- a | p) by auto with zarith.
+    apply H7, Zdivide_1 in H8; intuition.
   (* a = 0 *)
-  inversion H2. subst a; omega.
+  - inversion H1. subst a; omega.
   (* 1 < a < p *)
-  absurd (rel_prime a p); intuition.
-  inversion H3.
-  assert (a | a); auto with zarith.
-  assert (a | p); auto with zarith.
-  generalize (H8 a H9 H10); intuition idtac.
-  generalize (Zdivide_1 a H11); intuition.
+  - absurd (rel_prime a p); intuition.
+    inversion H2.
+    assert (a | a) by auto with zarith.
+    assert (a | p) by auto with zarith.
+    apply H7, Zdivide_1 in H8; intuition.
 Qed.
 
 (** A prime number is relatively prime with any number it does not divide *)
@@ -606,11 +605,10 @@ Qed.
 Lemma prime_rel_prime :
   forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
 Proof.
-  simple induction 1; intros.
-  constructor; intuition.
-  elim (prime_divisors p H x H3); intuition; subst; auto with zarith.
-  absurd (p | a); auto with zarith.
-  absurd (p | a); intuition.
+  intros; constructor; intros; auto with zarith.
+  apply prime_divisors in H1; intuition; subst; auto with zarith.
+  - absurd (p | a); auto with zarith.
+  - absurd (p | a); intuition.
 Qed.
 
 Hint Resolve prime_rel_prime: zarith.
@@ -635,7 +633,7 @@ Lemma prime_mult :
   forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).
 Proof.
   intro p; simple induction 1; intros.
-  case (Zdivide_dec p a); intuition.
+  case (Zdivide_dec p a); nintuition.
   right; apply Gauss with a; auto with zarith.
 Qed.