Renommage du IP classique pour éviter confusion avec IP constructif

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

1 files changed, 12 insertions, 12 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 723434512..5180bf5b2 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -23,19 +23,19 @@ Variables A B :Type.
 
 Definition RelationalChoice :=
   forall (R:A -> B -> Prop),
-    (forall x:A,  exists y : B, R x y) ->
+    (forall x:A, exists y : B, R x y) ->
      exists R' : A -> B -> Prop,
       (forall x:A,
-          exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
 Definition FunctionalChoice :=
   forall (R:A -> B -> Prop),
-    (forall x:A,  exists y : B, R x y) ->
+    (forall x:A, exists y : B, R x y) ->
      exists f : A -> B, (forall x:A, R x (f x)).
 
 Definition ParamDefiniteDescription :=
   forall (R:A -> B -> Prop),
-    (forall x:A,  exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
+    (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
      exists f : A -> B, (forall x:A, R x (f x)).
 
 Lemma description_rel_choice_imp_funct_choice :
@@ -92,11 +92,11 @@ End ChoiceEquivalences.
 
 Definition GuardedRelationalChoice (A B:Type) :=
   forall (P:A -> Prop) (R:A -> B -> Prop),
-    (forall x:A, P x ->  exists y : B, R x y) ->
+    (forall x:A, P x -> exists y : B, R x y) ->
      exists R' : A -> B -> Prop,
       (forall x:A,
          P x ->
-          exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
 Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
 
@@ -110,7 +110,7 @@ destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
 intros [x HPx].
 destruct (H x HPx) as [y HRxy].
 exists y; exact HRxy.
-set (R'' := fun (x:A) (y:B) =>  exists H : P x, R' (existT P x H) y).
+set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
 exists R''; intros x HPx.
 destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
 exists y. split.
@@ -125,13 +125,13 @@ exists y. split.
       exact HR'xy'.
 Qed.
 
-Definition IndependenceOfPremises :=
+Definition IndependenceOfGeneralPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
-    (Q ->  exists x : _, P x) ->  exists x : _, Q -> P x.
+    (Q -> exists x, P x) -> exists x, Q -> P x.
 
-Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
+Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
  forall A B, RelationalChoice A B -> 
-   IndependenceOfPremises -> GuardedRelationalChoice A B.
+   IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
 Proof.
 intros A B RelCh IndPrem.
 red in |- *; intros P R H.
@@ -200,7 +200,7 @@ destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
 Qed.
 
 Definition FunctionalChoice_on (A B:Type) (R:A->B->Prop) :=
-    (forall x:A,  exists y : B, R x y) ->
+    (forall x:A, exists y : B, R x y) ->
      exists f : A -> B, (forall x:A, R x (f x)).
 
 Lemma classical_denumerable_description_imp_fun_choice :