changement de pose en set (pose n'etait pas utilise avec la semantique

 documentee).
Reste a retablir la semantique de pose.


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

4 files changed, 7 insertions, 7 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index ca9bea5094..1ae9b9d5ed 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -103,7 +103,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.
-pose (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.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index a20036f0a5..d76d896585 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -45,7 +45,7 @@ Qed.
 Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
 Proof.
 intro HnotEM.
-pose (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
+set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
 assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
 apply description.
 intro A.
@@ -75,4 +75,4 @@ destruct (f P).
     discriminate.
     assumption.
 Qed.
- 
\ No newline at end of file
+ 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 0ece7ac76a..aa4960a35b 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -130,7 +130,7 @@ Lemma aux : prop_extensionality -> bool_dep_induction -> true = false.
 Proof.
 intros Ext Ind.
 case (ext_prop_fixpoint Ext bool true); intros G Gfix.
-pose (neg := fun b:bool => bool_elim bool false true b).
+set (neg := fun b:bool => bool_elim bool false true b).
 generalize (refl_equal (G neg)).
 pattern (G neg) at 1 in |- *.
 apply Ind with (b := G neg); intro Heq.
@@ -145,7 +145,7 @@ Lemma ext_prop_dep_proof_irrel_gen :
  prop_extensionality -> bool_dep_induction -> proof_irrelevance.
 Proof.
 intros Ext Ind A a1 a2.
-pose (f := fun b:bool => bool_elim A a1 a2 b).
+set (f := fun b:bool => bool_elim A a1 a2 b).
 rewrite (bool_elim_redl A a1 a2).
 change (f true = a2) in |- *.
 rewrite (bool_elim_redr A a1 a2).
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index e1fb12f398..03c31298f7 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -100,8 +100,8 @@ intro P.
 (* first we exhibit the choice functional relation R *)
 destruct AC as [R H].
 
-pose (class_of_true := fun b => b = true \/ P).
-pose (class_of_false := fun b => b = false \/ P).
+set (class_of_true := fun b => b = true \/ P).
+set (class_of_false := fun b => b = false \/ P).
 
 (* the actual "decision": is (R class_of_true) = true or false? *)
 destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].