diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-23 18:51:11 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-23 18:51:11 +0000 |
commit | 7e02b97b3017a5a3055fca8e0fc6e89f84b6a1c4 (patch) | |
tree | 1009560f396c397caa537471fc922aa0fb2af0bf /theories/Logic/ChoiceFacts.v | |
parent | e3567014035a55cfde44099ce59d142d084faac5 (diff) |
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
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
-rw-r--r-- | theories/Logic/ChoiceFacts.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 8d82bc8ea..02eadf091 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. |