MAJ changements ChoiceFacts

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

2 files changed, 9 insertions, 8 deletions

diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 0bc491e20..69887a540 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -23,10 +23,11 @@ Require Import ChoiceFacts.
 
 Theorem choice :
  forall (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)).
 Proof.
+intros A B.
 apply description_rel_choice_imp_funct_choice.
-exact description.
-exact relational_choice.
-Qed.
\ No newline at end of file
+exact (description A B).
+exact (relational_choice A B).
+Qed.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index d815b9dda..5f7112fd7 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -59,18 +59,18 @@ Qed.
 
 Require Import ChoiceFacts.
 
-Variable rel_choice : RelationalChoice.
+Variable rel_choice : forall A B:Type, RelationalChoice A B.
 
 Lemma guarded_rel_choice :
  forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
    (forall x:A, P x ->  exists y : B, R x y) ->
-    exists R' : A -> B -> Prop,
+     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')).
 Proof.
-  exact
-   (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
+ apply
+  (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
 Qed.
 
 (** The form of choice we need: there is a functional relation which chooses