remove undocumented and scarcely-used tactic auto decomp

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

2 files changed, 19 insertions, 19 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 24cbc3f93b..da1d9e9890 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -11,7 +11,7 @@ Require Import Plus.
 Require Import Compare_dec.
 Require Import Even.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Type n : nat.
 
@@ -69,24 +69,24 @@ Proof.
     (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
 Qed.
 
-Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
-with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
+Lemma div2_even n : div2 n = div2 (S n) -> even n
+with div2_odd n : S (div2 n) = div2 (S n) -> odd n.
 Proof.
-  destruct n; intro H.
-    (* 0 *) constructor.
-    (* S n *) constructor. apply div2_odd. rewrite H. trivial.
-  destruct n; intro H.
-    (* 0 *) discriminate.
-    (* S n *) constructor. apply div2_even. injection H as <-. trivial.
+{ destruct n; intro H.
+  - constructor.
+  - constructor. apply div2_odd. rewrite H. trivial. }
+{ destruct n; intro H.
+  - discriminate.
+  - constructor. apply div2_even. injection H as <-. trivial. }
 Qed.
 
 Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
-Lemma even_odd_div2 :
-  forall n,
-    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
+Lemma even_odd_div2 n :
+ (even n <-> div2 n = div2 (S n)) /\
+ (odd n <-> S (div2 n) = div2 (S n)).
 Proof.
-  auto decomp using div2_odd, div2_even, odd_div2, even_div2.
+ split; split; auto using div2_odd, div2_even, odd_div2, even_div2.
 Qed.
 
 
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 8d82bc8ea1..02eadf0916 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -385,7 +385,7 @@ Qed.
 Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice :
   ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice).
 Proof.
-  auto decomp using
+  intuition auto using
     guarded_rel_choice_imp_rel_choice,
     rel_choice_and_proof_irrel_imp_guarded_rel_choice.
 Qed.
@@ -439,7 +439,7 @@ Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice :
   FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises
   <-> GuardedFunctionalChoice.
 Proof.
-  auto decomp using
+  intuition auto using
     guarded_fun_choice_imp_indep_of_general_premises,
     guarded_fun_choice_imp_fun_choice,
     fun_choice_and_indep_general_prem_imp_guarded_fun_choice.
@@ -480,7 +480,7 @@ Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice :
   FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox
   <-> OmniscientFunctionalChoice.
 Proof.
-  auto decomp using
+  intuition auto using
     omniscient_fun_choice_imp_small_drinker,
     omniscient_fun_choice_imp_fun_choice,
     fun_choice_and_small_drinker_imp_omniscient_fun_choice.
@@ -547,7 +547,7 @@ Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon :
   (EpsilonStatement ->
    SmallDrinker'sParadox * ConstructiveIndefiniteDescription).
 Proof.
-  auto decomp using
+  intuition auto using
     epsilon_imp_constructive_indefinite_description,
     constructive_indefinite_description_and_small_drinker_imp_epsilon,
     epsilon_imp_small_drinker.
@@ -689,7 +689,7 @@ Qed.
 Corollary dep_iff_non_dep_functional_rel_reification :
   FunctionalRelReification <-> DependentFunctionalRelReification.
 Proof.
-  auto decomp using
+  intuition auto using
     non_dep_dep_functional_rel_reification,
     dep_non_dep_functional_rel_reification.
 Qed.
@@ -814,7 +814,7 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context :
   (forall P:Prop, P \/ ~ P) ->
   forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C.
 Proof.
-  intros FunReify EM C; auto decomp using
+  intros FunReify EM C; intuition auto using
     constructive_definite_descr_excluded_middle,
     (relative_non_contradiction_of_definite_descr (C:=C)).
 Qed.