Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

18 files changed, 786 insertions, 741 deletions

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 9f6217320..932db000f 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -31,62 +31,55 @@ Set Implicit Arguments.
 Section Berardis_paradox.
 
 (** Excluded middle *)
-Hypothesis EM : (P:Prop) P \/ ~P.
+Hypothesis EM : forall P:Prop, P \/ ~ P.
 
 (** Conditional on any proposition. *)
-Definition IFProp := [P,B:Prop][e1,e2:P]
-  Cases (EM B) of
-    (or_introl _) => e1
-  | (or_intror _) => e2
+Definition IFProp (P B:Prop) (e1 e2:P) :=
+  match EM B with
+  | or_introl _ => e1
+  | or_intror _ => e2
   end.
 
 (** Axiom of choice applied to disjunction.
     Provable in Coq because of dependent elimination. *)
-Lemma AC_IF : (P,B:Prop)(e1,e2:P)(Q:P->Prop)
-  ( B -> (Q e1))->
-  (~B -> (Q e2))->
-  (Q (IFProp B e1 e2)).
+Lemma AC_IF :
+ forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
+   (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
 Proof.
-Intros P B e1 e2 Q p1 p2.
-Unfold IFProp.
-Case (EM B); Assumption.
+intros P B e1 e2 Q p1 p2.
+unfold IFProp in |- *.
+case (EM B); assumption.
 Qed.
 
 
 (** We assume a type with two elements. They play the role of booleans.
     The main theorem under the current assumptions is that [T=F] *)
-Variable Bool: Prop.
-Variable T: Bool.
-Variable F: Bool.
+Variable Bool : Prop.
+Variable T : Bool.
+Variable F : Bool.
 
 (** The powerset operator *)
-Definition pow [P:Prop] :=P->Bool.
+Definition pow (P:Prop) := P -> Bool.
 
 
 (** A piece of theory about retracts *)
 Section Retracts.
 
-Variable A,B: Prop.
+Variables A B : Prop.
 
-Record retract : Prop := {
-    i: A->B;
-    j: B->A;
-    inv: (a:A)(j (i a))==a
-  }.
+Record retract : Prop := 
+  {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
 
-Record retract_cond : Prop := {
-    i2: A->B;
-    j2: B->A;
-    inv2: retract -> (a:A)(j2 (i2 a))==a
-  }.
+Record retract_cond : Prop := 
+  {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
 
 
 (** The dependent elimination above implies the axiom of choice: *)
-Lemma AC: (r:retract_cond) retract -> (a:A)((j2 r) ((i2 r) a))==a.
+Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
 Proof.
-Intros r.
-Case r; Simpl.
-Trivial.
+intros r.
+case r; simpl in |- *.
+trivial.
 Qed.
 
 End Retracts.
@@ -96,75 +89,71 @@ End Retracts.
     which is provable in classical logic ( => is already provable in
     intuitionnistic logic). *)
 
-Lemma L1 : (A,B:Prop)(retract_cond (pow A) (pow B)).
+Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
 Proof.
-Intros A B.
-Elim (EM (retract (pow A) (pow B))).
-Intros (f0, g0, e).
-Exists f0 g0.
-Trivial.
-
-Intros hf.
-Exists ([x:(pow A); y:B]F) ([x:(pow B); y:A]F).
-Intros; Elim hf; Auto.
+intros A B.
+elim (EM (retract (pow A) (pow B))).
+intros [f0 g0 e].
+exists f0 g0.
+trivial.
+
+intros hf.
+exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F).
+intros; elim hf; auto.
 Qed.
 
 
 (** The paradoxical set *)
-Definition U := (P:Prop)(pow P).
+Definition U := forall P:Prop, pow P.
 
 (** Bijection between [U] and [(pow U)] *)
-Definition f : U -> (pow U) :=
-  [u](u U).
+Definition f (u:U) : pow U := u U.
 
-Definition g : (pow U) -> U :=
-  [h,X]
-    let lX = (j2 (L1 X U)) in
-    let rU = (i2 (L1 U U)) in
-    (lX (rU h)).
+Definition g (h:pow U) : U :=
+  fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h).
 
 (** We deduce that the powerset of [U] is a retract of [U].
     This lemma is stated in Berardi's article, but is not used
     afterwards. *)
-Lemma retract_pow_U_U : (retract (pow U) U).
+Lemma retract_pow_U_U : retract (pow U) U.
 Proof.
-Exists g f.
-Intro a.
-Unfold f g; Simpl.
-Apply AC.
-Exists ([x:(pow U)]x) ([x:(pow U)]x).
-Trivial.
+exists g f.
+intro a.
+unfold f, g in |- *; simpl in |- *.
+apply AC.
+exists (fun x:pow U => x) (fun x:pow U => x).
+trivial.
 Qed.
 
 (** Encoding of Russel's paradox *)
 
 (** The boolean negation. *)
-Definition Not_b := [b:Bool](IFProp b==T F T).
+Definition Not_b (b:Bool) := IFProp (b = T) F T.
 
 (** the set of elements not belonging to itself *)
-Definition R : U := (g ([u:U](Not_b (u U u)))).
+Definition R : U := g (fun u:U => Not_b (u U u)).
 
 
-Lemma not_has_fixpoint : (R R)==(Not_b (R R)).
+Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
-Unfold 1 R.
-Unfold g.
-Rewrite AC with r:=(L1 U U) a:=[u:U](Not_b (u U u)).
-Trivial.
-Exists ([x:(pow U)]x) ([x:(pow U)]x); Trivial.
+unfold R at 1 in |- *.
+unfold g in |- *.
+rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
+trivial.
+exists (fun x:pow U => x) (fun x:pow U => x); trivial.
 Qed.
 
 
-Theorem classical_proof_irrelevence : T==F.
+Theorem classical_proof_irrelevence : T = F.
 Proof.
-Generalize not_has_fixpoint.
-Unfold Not_b.
-Apply AC_IF.
-Intros is_true is_false.
-Elim is_true; Elim is_false; Trivial.
-
-Intros not_true is_true.
-Elim not_true; Trivial.
+generalize not_has_fixpoint.
+unfold Not_b in |- *.
+apply AC_IF.
+intros is_true is_false.
+elim is_true; elim is_false; trivial.
+
+intros not_true is_true.
+elim not_true; trivial.
 Qed.
 
-End Berardis_paradox.
+End Berardis_paradox.
\ No newline at end of file
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 699051ec1..192603273 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -18,64 +18,66 @@
    though definite description conflicts with classical logic *)
 
 Definition RelationalChoice :=
- (A:Type;B:Type;R: A->B->Prop) 
-  ((x:A)(EX y:B|(R x y)))
-   -> (EXT R':A->B->Prop | 
-         ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))).
+  forall (A B:Type) (R:A -> B -> Prop),
+    (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')).
 
 Definition FunctionalChoice :=
- (A:Type;B:Type;R: A->B->Prop)
-  ((x:A)(EX y:B|(R x y))) -> (EX f:A->B | (x:A)(R x (f x))).
+  forall (A B:Type) (R:A -> B -> Prop),
+    (forall x:A,  exists y : B | R x y) ->
+     exists f : A -> B | (forall x:A, R x (f x)).
 
 Definition ParamDefiniteDescription :=
- (A:Type;B:Type;R: A->B->Prop)
-  ((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y')))
-   -> (EX f:A->B | (x:A)(R x (f x))).
-
-Lemma description_rel_choice_imp_funct_choice : 
-  ParamDefiniteDescription->RelationalChoice->FunctionalChoice.
-Intros Descr RelCh.
-Red; Intros A B R H.
-NewDestruct (RelCh A B R H) as [R' H0].
-NewDestruct (Descr A B R') as [f H1].
-Intro x.
-Elim (H0 x); Intros y [H2 [H3 H4]]; Exists y; Split; [Exact H3 | Exact H4].
-Exists f; Intro x.
-Elim (H0 x); Intros y [H2 [H3 H4]].
-Rewrite <- (H4 (f x) (H1 x)).
-Exact H2.
+  forall (A B:Type) (R:A -> B -> Prop),
+    (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 :
+ ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
+intros Descr RelCh.
+red in |- *; intros A B R H.
+destruct (RelCh A B R H) as [R' H0].
+destruct (Descr A B R') as [f H1].
+intro x.
+elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ].
+exists f; intro x.
+elim (H0 x); intros y [H2 [H3 H4]].
+rewrite <- (H4 (f x) (H1 x)).
+exact H2.
 Qed.
 
-Lemma funct_choice_imp_rel_choice : 
-  FunctionalChoice->RelationalChoice.
-Intros FunCh.
-Red; Intros A B R H.
-NewDestruct (FunCh A B R H) as [f H0].
-Exists [x,y]y=(f x).
-Intro x; Exists (f x);
-Split; [Apply H0| Split;[Reflexivity| Intros y H1; Symmetry; Exact H1]].
+Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
+intros FunCh.
+red in |- *; intros A B R H.
+destruct (FunCh A B R H) as [f H0].
+exists (fun x y => y = f x).
+intro x; exists (f x); split;
+ [ apply H0
+ | split; [ reflexivity | intros y H1; symmetry  in |- *; exact H1 ] ].
 Qed.
 
-Lemma funct_choice_imp_description : 
-  FunctionalChoice->ParamDefiniteDescription.
-Intros FunCh.
-Red; Intros A B R H.
-NewDestruct (FunCh A B R) as [f H0].
+Lemma funct_choice_imp_description :
+ FunctionalChoice -> ParamDefiniteDescription.
+intros FunCh.
+red in |- *; intros A B R H.
+destruct (FunCh A B R) as [f H0].
 (* 1 *)
-Intro x.
-Elim (H x); Intros y [H0 H1].
-Exists y; Exact H0.
+intro x.
+elim (H x); intros y [H0 H1].
+exists y; exact H0.
 (* 2 *)
-Exists f; Exact H0.
+exists f; exact H0.
 Qed.
 
 Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
-  FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
-Split.
-Intro H; Split; [
-  Exact (funct_choice_imp_rel_choice H)
- | Exact (funct_choice_imp_description H)].
-Intros [H H0]; Exact (description_rel_choice_imp_funct_choice H0 H).
+ FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
+split.
+intro H; split;
+ [ exact (funct_choice_imp_rel_choice H)
+ | exact (funct_choice_imp_description H) ].
+intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.
 
 (* We show that the guarded relational formulation of the axiom of Choice
@@ -83,52 +85,55 @@ Qed.
    independance of premises or proof-irrelevance *)
 
 Definition GuardedRelationalChoice :=
- (A:Type;B:Type;P:A->Prop;R: A->B->Prop) 
-  ((x:A)(P x)->(EX y:B|(R x y)))
-   -> (EXT R':A->B->Prop | 
-        ((x:A)(P x)->(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))).
+  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
+    | (forall x:A,
+         P x ->
+          exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
 
-Definition ProofIrrelevance := (A:Prop)(a1,a2:A) a1==a2.
+Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
 
-Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice : 
-  RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
+Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
+ RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
 Proof.
-Intros rel_choice proof_irrel.
-Red; Intros A B P R H.
-NewDestruct (rel_choice ? ? [x:(sigT ? P);y:B](R (projT1 ? ? x) y)) as [R' H0].
-Intros [x HPx].
-NewDestruct (H x HPx) as [y HRxy].
-Exists y; Exact HRxy.
-Pose R'':=[x:A;y:B](EXT H:(P x) | (R' (existT ? P x H) y)).
-Exists R''; Intros x HPx.
-NewDestruct (H0 (existT ? P x HPx)) as [y [HRxy [HR'xy Huniq]]].
-Exists y. Split.
-  Exact HRxy.
-  Split.
-    Red; Exists HPx; Exact HR'xy.
-    Intros y' HR''xy'.
-      Apply Huniq.
-      Unfold R'' in HR''xy'.
-      NewDestruct HR''xy' as [H'Px HR'xy'].
-      Rewrite proof_irrel with a1:=HPx a2:=H'Px.
-      Exact HR'xy'.
+intros rel_choice proof_irrel.
+red in |- *; intros A B P R H.
+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).
+exists R''; intros x HPx.
+destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
+exists y. split.
+  exact HRxy.
+  split.
+    red in |- *; exists HPx; exact HR'xy.
+    intros y' HR''xy'.
+      apply Huniq.
+      unfold R'' in HR''xy'.
+      destruct HR''xy' as [H'Px HR'xy'].
+      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px).
+      exact HR'xy'.
 Qed.
 
 Definition IndependenceOfPremises :=
- (A:Type)(P:A->Prop)(Q:Prop)(Q->(EXT x|(P x)))->(EXT x|Q->(P x)).
+  forall (A:Type) (P:A -> Prop) (Q:Prop),
+    (Q ->  exists x : _ | P x) ->  exists x : _ | Q -> P x.
 
 Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
-  RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
+ RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
 Proof.
-Intros RelCh IndPrem.
-Red; Intros A B P R H.
-NewDestruct (RelCh A B [x,y](P x)->(R x y)) as [R' H0].
-  Intro x. Apply IndPrem.
-    Apply H.
-  Exists R'.
-  Intros x HPx.
-    NewDestruct (H0 x) as [y [H1 H2]].
-    Exists y. Split. 
-      Apply (H1 HPx).
-      Exact H2.
-Qed.
+intros RelCh IndPrem.
+red in |- *; intros A B P R H.
+destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
+  intro x. apply IndPrem.
+    apply H.
+  exists R'.
+  intros x HPx.
+    destruct (H0 x) as [y [H1 H2]].
+    exists y. split. 
+      apply (H1 HPx).
+      exact H2.
+Qed.
\ No newline at end of file
diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v
index 324005caf..1f3b531af 100755
--- a/theories/Logic/Classical.v
+++ b/theories/Logic/Classical.v
@@ -11,4 +11,4 @@
 (** Classical Logic *)
 
 Require Export Classical_Prop.
-Require Export Classical_Pred_Type.
+Require Export Classical_Pred_Type.
\ No newline at end of file
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 31f58a95e..80bbce461 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -19,13 +19,14 @@
 
 Require Export ClassicalDescription.
 Require Export RelationalChoice.
-Require ChoiceFacts.
+Require Import ChoiceFacts.
 
-Theorem choice : 
- (A:Type;B:Type;R: A->B->Prop)
-  ((x:A)(EX y:B|(R x y))) -> (EX f:A->B | (x:A)(R x (f x))).
+Theorem choice :
+ forall (A B:Type) (R:A -> B -> Prop),
+   (forall x:A,  exists y : B | R x y) ->
+    exists f : A -> B | (forall x:A, R x (f x)).
 Proof.
-Apply description_rel_choice_imp_funct_choice.
-Exact description.
-Exact relational_choice.
-Qed.
+apply description_rel_choice_imp_funct_choice.
+exact description.
+exact relational_choice.
+Qed.
\ No newline at end of file
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index ea2f4f727..26e696a7c 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -22,55 +22,57 @@
 
 Require Export Classical.
 
-Axiom dependent_description :
-  (A:Type;B:A->Type;R: (x:A)(B x)->Prop)
-  ((x:A)(EX y:(B x)|(R x y)/\ ((y':(B x))(R x y') -> y=y')))
-   -> (EX f:(x:A)(B x) | (x:A)(R x (f x))).
+Axiom
+  dependent_description :
+    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+      (forall x:A,
+          exists y : B x | R x y /\ (forall y':B x, R x y' -> y = y')) ->
+       exists f : forall x:A, B x | (forall x:A, R x (f x)).
 
 (** Principle of definite description (aka axiom of unique choice) *)
 
 Theorem description :
-  (A:Type;B:Type;R: A->B->Prop)
-  ((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y')))
-   -> (EX f:A->B | (x:A)(R x (f x))).
+ forall (A B:Type) (R:A -> B -> Prop),
+   (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)).
 Proof.
-Intros A B.
-Apply (dependent_description A [_]B).
+intros A B.
+apply (dependent_description A (fun _ => B)).
 Qed.
 
 (** The followig proof comes from [1] *)
 
-Theorem classic_set : (((P:Prop){P}+{~P}) -> False) -> False.
+Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
 Proof.
-Intro HnotEM.
-Pose R:=[A,b]A/\true=b \/ ~A/\false=b.
-Assert H:(EX f:Prop->bool|(A:Prop)(R A (f A))).
-Apply description.
-Intro A.
-NewDestruct (classic A) as [Ha|Hnota].
-  Exists true; Split.
-    Left; Split; [Assumption|Reflexivity].
-    Intros y [[_ Hy]|[Hna _]].
-      Assumption.
-      Contradiction.
-  Exists false; Split.
-    Right; Split; [Assumption|Reflexivity].
-    Intros y [[Ha _]|[_ Hy]].
-      Contradiction.
-      Assumption.
-NewDestruct H as [f Hf].
-Apply HnotEM.
-Intro P.
-Assert HfP := (Hf P).
+intro HnotEM.
+pose (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.
+destruct (classic A) as [Ha| Hnota].
+  exists true; split.
+    left; split; [ assumption | reflexivity ].
+    intros y [[_ Hy]| [Hna _]].
+      assumption.
+      contradiction.
+  exists false; split.
+    right; split; [ assumption | reflexivity ].
+    intros y [[Ha _]| [_ Hy]].
+      contradiction.
+      assumption.
+destruct H as [f Hf].
+apply HnotEM.
+intro P.
+assert (HfP := Hf P).
 (* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
-NewDestruct (f P).
-  Left.
-  NewDestruct HfP as [[Ha _]|[_ Hfalse]].
-    Assumption.
-    Discriminate.
-  Right.
-  NewDestruct HfP as [[_ Hfalse]|[Hna _]].
-    Discriminate.
-    Assumption.
+destruct (f P).
+  left.
+  destruct HfP as [[Ha _]| [_ Hfalse]].
+    assumption.
+    discriminate.
+  right.
+  destruct HfP as [[_ Hfalse]| [Hna _]].
+    discriminate.
+    assumption.
 Qed.
- 
+ 
\ No newline at end of file
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 622e6959d..0ece7ac76 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -12,49 +12,50 @@
 
 (** [prop_degeneracy] asserts (up to consistency) that there are only *)
 (*  two distinct formulas *)
-Definition prop_degeneracy := (A:Prop) A==True \/ A==False.
+Definition prop_degeneracy := forall A:Prop, A = True \/ A = False.
 
 (** [prop_extensionality] asserts equivalent formulas are equal *)
-Definition prop_extensionality := (A,B:Prop) (A<->B) -> A==B.
+Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B.
 
 (** [excluded_middle] asserts we can reason by case on the truth *)
 (*  or falsity of any formula *)
-Definition excluded_middle := (A:Prop) A \/ ~A.
+Definition excluded_middle := forall A:Prop, A \/ ~ A.
 
 (** [proof_irrelevance] asserts equality of all proofs of a given formula *)
-Definition proof_irrelevance := (A:Prop)(a1,a2:A) a1==a2.
+Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
 
 (** We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *)
 
 Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality.
 Proof.
-Intros H A B (Hab,Hba).
-NewDestruct (H A); NewDestruct (H B).
-  Rewrite H1; Exact H0.
-  Absurd B.
-    Rewrite H1; Exact [H]H.
-    Apply Hab; Rewrite H0; Exact I.
-  Absurd A.
-    Rewrite H0; Exact [H]H.
-    Apply Hba; Rewrite H1; Exact I.
-  Rewrite H1; Exact H0.
+intros H A B [Hab Hba].
+destruct (H A); destruct (H B).
+  rewrite H1; exact H0.
+  absurd B.
+    rewrite H1; exact (fun H => H).
+    apply Hab; rewrite H0; exact I.
+  absurd A.
+    rewrite H0; exact (fun H => H).
+    apply Hba; rewrite H1; exact I.
+  rewrite H1; exact H0.
 Qed.
 
 Lemma prop_degen_em : prop_degeneracy -> excluded_middle.
 Proof.
-Intros H A.
-NewDestruct (H A).
-  Left; Rewrite H0; Exact I.
-  Right; Rewrite H0; Exact [x]x.
+intros H A.
+destruct (H A).
+  left; rewrite H0; exact I.
+  right; rewrite H0; exact (fun x => x).
 Qed.
 
 Lemma prop_ext_em_degen :
-   prop_extensionality -> excluded_middle -> prop_degeneracy.
+ prop_extensionality -> excluded_middle -> prop_degeneracy.
 Proof.
-Intros Ext EM A.
-NewDestruct (EM A).
-  Left; Apply (Ext A True); Split; [Exact [_]I | Exact [_]H].
-  Right; Apply (Ext A False); Split; [Exact H | Apply False_ind].
+intros Ext EM A.
+destruct (EM A).
+  left; apply (Ext A True); split;
+   [ exact (fun _ => I) | exact (fun _ => H) ].
+  right; apply (Ext A False); split; [ exact H | apply False_ind ].
 Qed.
 
 (** We successively show that:
@@ -67,45 +68,40 @@ Qed.
         (e.g. take the Y combinator of lambda-calculus)
 *)
 
-Definition inhabited [A:Prop] := A.
+Definition inhabited (A:Prop) := A.
 
 Lemma prop_ext_A_eq_A_imp_A :
-  prop_extensionality->(A:Prop)(inhabited A)->(A->A)==A.
+ prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
 Proof.
-Intros Ext A a.
-Apply (Ext A->A A); Split; [ Exact [_]a | Exact [_;_]a ].
+intros Ext A a.
+apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ].
 Qed.
 
-Record retract [A,B:Prop] : Prop := {
-  f1: A->B;
-  f2: B->A;
-  f1_o_f2: (x:B)(f1 (f2 x))==x
-}.
+Record retract (A B:Prop) : Prop := 
+  {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}.
 
 Lemma prop_ext_retract_A_A_imp_A :
-  prop_extensionality->(A:Prop)(inhabited A)->(retract A A->A).
+ prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A).
 Proof.
-Intros Ext A a.
-Rewrite -> (prop_ext_A_eq_A_imp_A Ext A a).
-Exists [x:A]x [x:A]x.
-Reflexivity.
+intros Ext A a.
+rewrite (prop_ext_A_eq_A_imp_A Ext A a).
+exists (fun x:A => x) (fun x:A => x).
+reflexivity.
 Qed.
 
-Record has_fixpoint [A:Prop] : Prop := {
-  F : (A->A)->A;
-  fix : (f:A->A)(F f)==(f (F f))
-}.
+Record has_fixpoint (A:Prop) : Prop := 
+  {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}.
 
 Lemma ext_prop_fixpoint :
-  prop_extensionality->(A:Prop)(inhabited A)->(has_fixpoint A).
+ prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A.
 Proof.
-Intros Ext A a.
-Case (prop_ext_retract_A_A_imp_A Ext A a); Intros g1 g2 g1_o_g2.
-Exists [f]([x:A](f (g1 x x)) (g2 [x](f (g1 x x)))).
-Intro f.
-Pattern 1 (g1 (g2 [x:A](f (g1 x x)))).
-Rewrite (g1_o_g2 [x:A](f (g1 x x))).
-Reflexivity.
+intros Ext A a.
+case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2.
+exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))).
+intro f.
+pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *.
+rewrite (g1_o_g2 (fun x:A => f (g1 x x))).
+reflexivity.
 Qed.
 
 (** Assume we have booleans with the property that there is at most 2
@@ -122,36 +118,40 @@ Section Proof_irrelevance_gen.
 Variable bool : Prop.
 Variable true : bool.
 Variable false : bool.
-Hypothesis bool_elim : (C:Prop)C->C->bool->C.
-Hypothesis bool_elim_redl : (C:Prop)(c1,c2:C)c1==(bool_elim C c1 c2 true).
-Hypothesis bool_elim_redr : (C:Prop)(c1,c2:C)c2==(bool_elim C c1 c2 false).
-Local bool_dep_induction := (P:bool->Prop)(P true)->(P false)->(b:bool)(P b).
-
-Lemma aux : prop_extensionality -> bool_dep_induction -> true==false.
+Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C.
+Hypothesis
+  bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true.
+Hypothesis
+  bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false.
+Let bool_dep_induction :=
+  forall P:bool -> Prop, P true -> P false -> forall b:bool, P b.
+
+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 := [b:bool](bool_elim bool false true b).
-Generalize (refl_eqT ? (G neg)).
-Pattern 1 (G neg).
-Apply Ind with b:=(G neg); Intro Heq.
-Rewrite (bool_elim_redl bool false true).
-Change true==(neg true); Rewrite -> Heq; Apply Gfix.
-Rewrite (bool_elim_redr bool false true).
-Change (neg false)==false; Rewrite -> Heq; Symmetry; Apply Gfix.
+intros Ext Ind.
+case (ext_prop_fixpoint Ext bool true); intros G Gfix.
+pose (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.
+rewrite (bool_elim_redl bool false true).
+change (true = neg true) in |- *; rewrite Heq; apply Gfix.
+rewrite (bool_elim_redr bool false true).
+change (neg false = false) in |- *; rewrite Heq; symmetry  in |- *;
+ apply Gfix.
 Qed.
 
 Lemma ext_prop_dep_proof_irrel_gen :
-  prop_extensionality -> bool_dep_induction -> proof_irrelevance.
+ prop_extensionality -> bool_dep_induction -> proof_irrelevance.
 Proof.
-Intros Ext Ind A a1 a2.
-Pose f := [b:bool](bool_elim A a1 a2 b).
-Rewrite (bool_elim_redl A a1 a2).
-Change (f true)==a2.
-Rewrite (bool_elim_redr A a1 a2).
-Change (f true)==(f false).
-Rewrite (aux Ext Ind).
-Reflexivity.
+intros Ext Ind A a1 a2.
+pose (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).
+change (f true = f false) in |- *.
+rewrite (aux Ext Ind).
+reflexivity.
 Qed.
 
 End Proof_irrelevance_gen.
@@ -163,22 +163,23 @@ End Proof_irrelevance_gen.
 
 Section Proof_irrelevance_CC.
 
-Definition BoolP  := (C:Prop)C->C->C.
-Definition TrueP  := [C][c1,c2]c1 : BoolP.
-Definition FalseP := [C][c1,c2]c2 : BoolP.
-Definition BoolP_elim := [C][c1,c2][b:BoolP](b C c1 c2).
-Definition BoolP_elim_redl : (C:Prop)(c1,c2:C)c1==(BoolP_elim C c1 c2 TrueP)
-  := [C;c1,c2](refl_eqT C c1).
-Definition BoolP_elim_redr : (C:Prop)(c1,c2:C)c2==(BoolP_elim C c1 c2 FalseP)
-  := [C;c1,c2](refl_eqT C c2).
+Definition BoolP := forall C:Prop, C -> C -> C.
+Definition TrueP : BoolP := fun C c1 c2 => c1.
+Definition FalseP : BoolP := fun C c1 c2 => c2.
+Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2.
+Definition BoolP_elim_redl (C:Prop) (c1 c2:C) :
+  c1 = BoolP_elim C c1 c2 TrueP := refl_equal c1.
+Definition BoolP_elim_redr (C:Prop) (c1 c2:C) :
+  c2 = BoolP_elim C c1 c2 FalseP := refl_equal c2.
 
-Definition BoolP_dep_induction := 
- (P:BoolP->Prop)(P TrueP)->(P FalseP)->(b:BoolP)(P b).
+Definition BoolP_dep_induction :=
+  forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b.
 
 Lemma ext_prop_dep_proof_irrel_cc :
-  prop_extensionality -> BoolP_dep_induction -> proof_irrelevance.
-Proof (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim
-         BoolP_elim_redl BoolP_elim_redr).
+ prop_extensionality -> BoolP_dep_induction -> proof_irrelevance.
+Proof
+  ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl
+    BoolP_elim_redr.
 
 End Proof_irrelevance_CC.
 
@@ -189,16 +190,20 @@ End Proof_irrelevance_CC.
 
 Section Proof_irrelevance_CIC.
 
-Inductive boolP : Prop := trueP : boolP | falseP : boolP.
-Definition boolP_elim_redl : (C:Prop)(c1,c2:C)c1==(boolP_ind C c1 c2 trueP)
-  := [C;c1,c2](refl_eqT C c1).
-Definition boolP_elim_redr : (C:Prop)(c1,c2:C)c2==(boolP_ind C c1 c2 falseP)
-  := [C;c1,c2](refl_eqT C c2).
+Inductive boolP : Prop :=
+  | trueP : boolP
+  | falseP : boolP.
+Definition boolP_elim_redl (C:Prop) (c1 c2:C) :
+  c1 = boolP_ind C c1 c2 trueP := refl_equal c1.
+Definition boolP_elim_redr (C:Prop) (c1 c2:C) :
+  c2 = boolP_ind C c1 c2 falseP := refl_equal c2.
 Scheme boolP_indd := Induction for boolP Sort Prop.
 
 Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance.
-Proof [pe](ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind
-         boolP_elim_redl boolP_elim_redr pe boolP_indd).
+Proof
+  fun pe =>
+    ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl
+      boolP_elim_redr pe boolP_indd.
 
 End Proof_irrelevance_CIC.
 
@@ -211,4 +216,4 @@ End Proof_irrelevance_CIC.
   satisfy propositional degeneracy without satisfying proof-irrelevance
   (nor dependent case analysis). This would imply that the previous
   results cannot be refined.
-*)
+*)
\ No newline at end of file
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index 7ca160517..e308eff14 100755
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -10,55 +10,61 @@
 
 (** Classical Predicate Logic on Set*)
 
-Require Classical_Prop.
+Require Import Classical_Prop.
 
 Section Generic.
-Variable U: Set.
+Variable U : Set.
 
 (** de Morgan laws for quantifiers *)
 
-Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EX n:U | ~(P n)).
+Lemma not_all_ex_not :
+ forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U | ~ P n.
 Proof.
-Unfold not; Intros P notall.
-Apply NNPP; Unfold not.
-Intro abs.
-Cut ((n:U)(P n)); Auto.
-Intro n; Apply NNPP.
-Unfold not; Intros.
-Apply abs; Exists n; Trivial.
+unfold not in |- *; intros P notall.
+apply NNPP; unfold not in |- *.
+intro abs.
+cut (forall n:U, P n); auto.
+intro n; apply NNPP.
+unfold not in |- *; intros.
+apply abs; exists n; trivial.
 Qed.
 
-Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EX n:U |(P n)).
+Lemma not_all_not_ex :
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U | P n.
 Proof.
-Intros P H.
-Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n.
-Apply NNPP; Trivial.
+intros P H.
+elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
+apply NNPP; trivial.
 Qed.
 
-Lemma not_ex_all_not : (P:U->Prop) (~(EX n:U |(P n))) -> (n:U)~(P n).
+Lemma not_ex_all_not :
+ forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n.
 Proof.
-Unfold not; Intros P notex n abs.
-Apply notex.
-Exists n; Trivial.
+unfold not in |- *; intros P notex n abs.
+apply notex.
+exists n; trivial.
 Qed. 
 
-Lemma not_ex_not_all : (P:U->Prop)(~(EX n:U | ~(P n))) -> (n:U)(P n).
+Lemma not_ex_not_all :
+ forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n.
 Proof.
-Intros P H n.
-Apply NNPP.
-Red; Intro K; Apply H; Exists n; Trivial.
+intros P H n.
+apply NNPP.
+red in |- *; intro K; apply H; exists n; trivial.
 Qed.
 
-Lemma ex_not_not_all : (P:U->Prop) (EX n:U | ~(P n)) -> ~(n:U)(P n).
+Lemma ex_not_not_all :
+ forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n).
 Proof.
-Unfold not; Intros P exnot allP.
-Elim exnot; Auto.
+unfold not in |- *; intros P exnot allP.
+elim exnot; auto.
 Qed.
 
-Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EX n:U |(P n)).
+Lemma all_not_not_ex :
+ forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n).
 Proof.
-Unfold not; Intros P allnot exP; Elim exP; Intros n p.
-Apply allnot with n; Auto.
+unfold not in |- *; intros P allnot exP; elim exP; intros n p.
+apply allnot with n; auto.
 Qed.
 
-End Generic.
+End Generic.
\ No newline at end of file
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 6745d05fd..6bfd08e43 100755
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -10,55 +10,61 @@
 
 (** Classical Predicate Logic on Type *)
 
-Require Classical_Prop.
+Require Import Classical_Prop.
 
 Section Generic.
-Variable U: Type.
+Variable U : Type.
 
 (** de Morgan laws for quantifiers *)
 
-Lemma not_all_ex_not : (P:U->Prop)(~(n:U)(P n)) -> (EXT n:U | ~(P n)).
+Lemma not_all_ex_not :
+ forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U | ~ P n.
 Proof.
-Unfold not; Intros P notall.
-Apply NNPP; Unfold not.
-Intro abs.
-Cut ((n:U)(P n)); Auto.
-Intro n; Apply NNPP.
-Unfold not; Intros.
-Apply abs; Exists n; Trivial.
+unfold not in |- *; intros P notall.
+apply NNPP; unfold not in |- *.
+intro abs.
+cut (forall n:U, P n); auto.
+intro n; apply NNPP.
+unfold not in |- *; intros.
+apply abs; exists n; trivial.
 Qed.
 
-Lemma not_all_not_ex : (P:U->Prop)(~(n:U)~(P n)) -> (EXT n:U | (P n)).
+Lemma not_all_not_ex :
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U | P n.
 Proof.
-Intros P H.
-Elim (not_all_ex_not [n:U]~(P n) H); Intros n Pn; Exists n.
-Apply NNPP; Trivial.
+intros P H.
+elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
+apply NNPP; trivial.
 Qed.
 
-Lemma not_ex_all_not : (P:U->Prop)(~(EXT n:U | (P n))) -> (n:U)~(P n).
+Lemma not_ex_all_not :
+ forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n.
 Proof.
-Unfold not; Intros P notex n abs.
-Apply notex.
-Exists n; Trivial.
+unfold not in |- *; intros P notex n abs.
+apply notex.
+exists n; trivial.
 Qed. 
 
-Lemma not_ex_not_all : (P:U->Prop)(~(EXT n:U | ~(P n))) -> (n:U)(P n).
+Lemma not_ex_not_all :
+ forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n.
 Proof.
-Intros P H n.
-Apply NNPP.
-Red; Intro K; Apply H; Exists n; Trivial.
+intros P H n.
+apply NNPP.
+red in |- *; intro K; apply H; exists n; trivial.
 Qed.
 
-Lemma ex_not_not_all : (P:U->Prop) (EXT n:U | ~(P n)) -> ~(n:U)(P n).
+Lemma ex_not_not_all :
+ forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n).
 Proof.
-Unfold not; Intros P exnot allP.
-Elim exnot; Auto.
+unfold not in |- *; intros P exnot allP.
+elim exnot; auto.
 Qed.
 
-Lemma all_not_not_ex : (P:U->Prop) ((n:U)~(P n)) -> ~(EXT n:U | (P n)).
+Lemma all_not_not_ex :
+ forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n).
 Proof.
-Unfold not; Intros P allnot exP; Elim exP; Intros n p.
-Apply allnot with n; Auto.
+unfold not in |- *; intros P allnot exP; elim exP; intros n p.
+apply allnot with n; auto.
 Qed.
 
-End Generic.
+End Generic.
\ No newline at end of file
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 0a5987d01..908ad40a2 100755
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -10,76 +10,76 @@
 
 (** Classical Propositional Logic *)
 
-Require ProofIrrelevance.
+Require Import ProofIrrelevance.
 
-Hints Unfold not : core.
+Hint Unfold not: core.
 
-Axiom classic: (P:Prop)(P \/ ~(P)).
+Axiom classic : forall P:Prop, P \/ ~ P.
 
-Lemma NNPP : (p:Prop)~(~(p))->p.
+Lemma NNPP : forall p:Prop, ~ ~ p -> p.
 Proof.
-Unfold not; Intros; Elim (classic p); Auto.
-Intro NP; Elim (H NP).
+unfold not in |- *; intros; elim (classic p); auto.
+intro NP; elim (H NP).
 Qed.
 
-Lemma not_imply_elim : (P,Q:Prop)~(P->Q)->P.
+Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P.
 Proof.
-Intros; Apply NNPP; Red.
-Intro; Apply H; Intro; Absurd P; Trivial.
+intros; apply NNPP; red in |- *.
+intro; apply H; intro; absurd P; trivial.
 Qed.
 
-Lemma not_imply_elim2 : (P,Q:Prop)~(P->Q) -> ~Q.
+Lemma not_imply_elim2 : forall P Q:Prop, ~ (P -> Q) -> ~ Q.
 Proof.
-Intros; Elim (classic Q); Auto.
+intros; elim (classic Q); auto.
 Qed.
 
-Lemma imply_to_or : (P,Q:Prop)(P->Q) -> ~P \/ Q.
+Lemma imply_to_or : forall P Q:Prop, (P -> Q) -> ~ P \/ Q.
 Proof.
-Intros; Elim (classic P); Auto.
+intros; elim (classic P); auto.
 Qed.
 
-Lemma imply_to_and : (P,Q:Prop)~(P->Q) -> P /\ ~Q.
+Lemma imply_to_and : forall P Q:Prop, ~ (P -> Q) -> P /\ ~ Q.
 Proof.
-Intros; Split.
-Apply not_imply_elim with Q;  Trivial.
-Apply not_imply_elim2 with P; Trivial.
+intros; split.
+apply not_imply_elim with Q; trivial.
+apply not_imply_elim2 with P; trivial.
 Qed.
 
-Lemma or_to_imply : (P,Q:Prop)(~P \/ Q) -> P->Q.
+Lemma or_to_imply : forall P Q:Prop, ~ P \/ Q -> P -> Q.
 Proof.
-Induction 1; Auto.
-Intros H1 H2; Elim (H1 H2).
+simple induction 1; auto.
+intros H1 H2; elim (H1 H2).
 Qed.
 
-Lemma not_and_or : (P,Q:Prop)~(P/\Q)-> ~P \/ ~Q.
+Lemma not_and_or : forall P Q:Prop, ~ (P /\ Q) -> ~ P \/ ~ Q.
 Proof.
-Intros; Elim (classic P); Auto.
+intros; elim (classic P); auto.
 Qed.
 
-Lemma or_not_and : (P,Q:Prop)(~P \/ ~Q) -> ~(P/\Q).
+Lemma or_not_and : forall P Q:Prop, ~ P \/ ~ Q -> ~ (P /\ Q).
 Proof.
-Induction 1; Red; Induction 2; Auto.
+simple induction 1; red in |- *; simple induction 2; auto.
 Qed.
 
-Lemma not_or_and : (P,Q:Prop)~(P\/Q)-> ~P /\ ~Q.
+Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q.
 Proof.
-Intros; Elim (classic P); Auto.
+intros; elim (classic P); auto.
 Qed.
 
-Lemma and_not_or : (P,Q:Prop)(~P /\ ~Q) -> ~(P\/Q).
+Lemma and_not_or : forall P Q:Prop, ~ P /\ ~ Q -> ~ (P \/ Q).
 Proof.
-Induction 1; Red; Induction 3; Trivial.
+simple induction 1; red in |- *; simple induction 3; trivial.
 Qed.
 
-Lemma imply_and_or: (P,Q:Prop)(P->Q) -> P \/ Q -> Q.
+Lemma imply_and_or : forall P Q:Prop, (P -> Q) -> P \/ Q -> Q.
 Proof.
-Induction 2; Trivial.
+simple induction 2; trivial.
 Qed.
 
-Lemma imply_and_or2: (P,Q,R:Prop)(P->Q) -> P \/ R -> Q \/ R.
+Lemma imply_and_or2 : forall P Q R:Prop, (P -> Q) -> P \/ R -> Q \/ R.
 Proof.
-Induction 2; Auto.
+simple induction 2; auto.
 Qed.
 
-Lemma proof_irrelevance: (P:Prop)(p1,p2:P)p1==p2.
-Proof (proof_irrelevance_cci classic).
+Lemma proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
+Proof proof_irrelevance_cci classic.
\ No newline at end of file
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
index 243daa9c4..acb7beac0 100755
--- a/theories/Logic/Classical_Type.v
+++ b/theories/Logic/Classical_Type.v
@@ -11,4 +11,4 @@
 (** Classical Logic for Type *)
 
 Require Export Classical_Prop.
-Require Export Classical_Pred_Type.
+Require Export Classical_Pred_Type.
\ No newline at end of file
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 82464b3af..ebc21f755 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -9,50 +9,52 @@
 
 (** Properties of decidable propositions *)
 
-Definition decidable := [P:Prop] P \/ ~P.
+Definition decidable (P:Prop) := P \/ ~ P.
 
-Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P.
-Unfold decidable; Tauto. 
+Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P.
+unfold decidable in |- *; tauto. 
 Qed.
 
-Theorem dec_True: (decidable True).
-Unfold decidable; Auto.
+Theorem dec_True : decidable True.
+unfold decidable in |- *; auto.
 Qed.
 
-Theorem dec_False: (decidable False).
-Unfold decidable not; Auto.
+Theorem dec_False : decidable False.
+unfold decidable, not in |- *; auto.
 Qed.
 
-Theorem dec_or: (A,B:Prop)(decidable A) -> (decidable B) -> (decidable (A\/B)).
-Unfold decidable; Tauto. 
+Theorem dec_or :
+ forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B).
+unfold decidable in |- *; tauto. 
 Qed.
 
-Theorem dec_and: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A/\B)).
-Unfold decidable; Tauto. 
+Theorem dec_and :
+ forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B).
+unfold decidable in |- *; tauto. 
 Qed.
 
-Theorem dec_not: (A:Prop)(decidable A) -> (decidable ~A).
-Unfold decidable; Tauto. 
+Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A).
+unfold decidable in |- *; tauto. 
 Qed.
 
-Theorem dec_imp: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A->B)).
-Unfold decidable; Tauto. 
+Theorem dec_imp :
+ forall A B:Prop, decidable A -> decidable B -> decidable (A -> B).
+unfold decidable in |- *; tauto. 
 Qed.
 
-Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P.
-Unfold decidable; Tauto. Qed.
+Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P.
+unfold decidable in |- *; tauto. Qed.
 
-Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B.
-Tauto. Qed.
+Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B.
+tauto. Qed.
 
-Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B.
-Unfold decidable; Tauto. Qed.
+Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B.
+unfold decidable in |- *; tauto. Qed.
 
-Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B.
-Unfold decidable;Tauto.
+Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B.
+unfold decidable in |- *; tauto.
 Qed.
 
-Theorem imp_simp : (A,B:Prop) (decidable A) -> (A -> B) -> ~A \/ B.
-Unfold decidable; Tauto.
+Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B.
+unfold decidable in |- *; tauto.
 Qed.
-
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index ff94d8e3b..b03ec80e8 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -30,104 +30,109 @@ Section PredExt_GuardRelChoice_imp_EM.
 (* The axiom of extensionality for predicates *)
 
 Definition PredicateExtensionality :=
-   (P,Q:bool->Prop)((b:bool)(P b)<->(Q b))->P==Q.
+  forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
 
 (* From predicate extensionality we get propositional extensionality
    hence proof-irrelevance *)
 
-Require ClassicalFacts.
+Require Import ClassicalFacts.
 
 Variable pred_extensionality : PredicateExtensionality.
   
-Lemma prop_ext : (A,B:Prop) (A<->B) -> A==B.
+Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
 Proof.
-  Intros A B H.
-  Change ([_]A true)==([_]B true).
-  Rewrite pred_extensionality with P:=[_:bool]A Q:=[_:bool]B.
-    Reflexivity.
-    Intros _; Exact H.
+  intros A B H.
+  change ((fun _ => A) true = (fun _ => B) true) in |- *.
+  rewrite
+   pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).
+    reflexivity.
+    intros _; exact H.
 Qed.
 
-Lemma proof_irrel : (A:Prop)(a1,a2:A) a1==a2.
+Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.
 Proof.
-  Apply (ext_prop_dep_proof_irrel_cic prop_ext).
+  apply (ext_prop_dep_proof_irrel_cic prop_ext).
 Qed.
 
 (* From proof-irrelevance and relational choice, we get guarded
    relational choice *)
 
-Require ChoiceFacts.
+Require Import ChoiceFacts.
 
 Variable rel_choice : RelationalChoice.
 
 Lemma guarded_rel_choice :
-  (A:Type)(B:Type)(P:A->Prop)(R:A->B->Prop)
-  ((x:A)(P x)->(EX y:B|(R x y)))->
-    (EXT R':A->B->Prop | 
-      ((x:A)(P x)->(EX y:B|(R x y)/\(R' x y)/\ ((y':B)(R' x y') -> y=y')))).
+ 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
+   | (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).
+  exact
+   (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
    an element in any non empty subset of bool *)
 
-Require Bool.
+Require Import Bool.
 
 Lemma AC :
-  (EXT R:(bool->Prop)->bool->Prop |
-     (P:bool->Prop)(EX b : bool | (P b))->
-        (EX b : bool | (P b) /\ (R P b) /\ ((b':bool)(R P b')->b=b'))).
+  exists R : (bool -> Prop) -> bool -> Prop
+ | (forall P:bool -> Prop,
+      ( exists b : bool | P b) ->
+       exists b : bool | P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
 Proof.
-  Apply guarded_rel_choice with
-    P:= [Q:bool->Prop](EX y | (Q y)) R:=[Q:bool->Prop;y:bool](Q y).
-  Exact [_;H]H.
+  apply guarded_rel_choice with
+   (P := fun Q:bool -> Prop =>  exists y : _ | Q y)
+   (R := fun (Q:bool -> Prop) (y:bool) => Q y).
+  exact (fun _ H => H).
 Qed.
 
 (* The proof of the excluded middle *)
 (* Remark: P could have been in Set or Type *)
 
-Theorem pred_ext_and_rel_choice_imp_EM : (P:Prop)P\/~P.
+Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
 Proof.
-Intro P.
+intro P.
 
 (* first we exhibit the choice functional relation R *)
-NewDestruct AC as [R H].
+destruct AC as [R H].
 
-Pose class_of_true := [b]b=true\/P.
-Pose class_of_false := [b]b=false\/P.
+pose (class_of_true := fun b => b = true \/ P).
+pose (class_of_false := fun b => b = false \/ P).
 
 (* the actual "decision": is (R class_of_true) = true or false? *)
-NewDestruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
-Exists true; Left; Reflexivity.
-NewDestruct H0.
+destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
+exists true; left; reflexivity.
+destruct H0.
 
 (* the actual "decision": is (R class_of_false) = true or false? *)
-NewDestruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
-Exists false; Left; Reflexivity.
-NewDestruct H1.
+destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
+exists false; left; reflexivity.
+destruct H1.
 
 (* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
-Right.
-Intro HP.
-Assert Hequiv:(b:bool)(class_of_true b)<->(class_of_false b).
-Intro b; Split.
-Unfold class_of_false; Right; Assumption.
-Unfold class_of_true; Right; Assumption.
-Assert Heq:class_of_true==class_of_false.
-Apply pred_extensionality with 1:=Hequiv.
-Apply diff_true_false.
-Rewrite <- H0.
-Rewrite <- H1.
-Rewrite <- H0''. Reflexivity.
-Rewrite Heq.
-Assumption.
+right.
+intro HP.
+assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
+intro b; split.
+unfold class_of_false in |- *; right; assumption.
+unfold class_of_true in |- *; right; assumption.
+assert (Heq : class_of_true = class_of_false).
+apply pred_extensionality with (1 := Hequiv).
+apply diff_true_false.
+rewrite <- H0.
+rewrite <- H1.
+rewrite <- H0''. reflexivity.
+rewrite Heq.
+assumption.
 
 (* cases where P is true *)
-Left; Assumption.
-Left; Assumption.
+left; assumption.
+left; assumption.
 
 Qed.
 
-End PredExt_GuardRelChoice_imp_EM.
+End PredExt_GuardRelChoice_imp_EM.
\ No newline at end of file
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 40a50837d..c5afa683a 100755
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -32,67 +32,68 @@
 Section Dependent_Equality.
 
 Variable U : Type.
-Variable P : U->Type.
+Variable P : U -> Type.
 
 (** Dependent equality *)
 
-Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop :=
-   eq_dep_intro : (eq_dep p x p x).
-Hint constr_eq_dep : core v62 := Constructors eq_dep.
+Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
+    eq_dep_intro : eq_dep p x p x.
+Hint Constructors eq_dep: core v62.
 
-Lemma eq_dep_sym : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep q y p x).
+Lemma eq_dep_sym :
+ forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x.
 Proof.
-Induction 1; Auto.
+simple induction 1; auto.
 Qed.
-Hints Immediate eq_dep_sym : core v62.
+Hint Immediate eq_dep_sym: core v62.
 
-Lemma eq_dep_trans : (p,q,r:U)(x:(P p))(y:(P q))(z:(P r))
-     (eq_dep p x q y)->(eq_dep q y r z)->(eq_dep p x r z).
+Lemma eq_dep_trans :
+ forall (p q r:U) (x:P p) (y:P q) (z:P r),
+   eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z.
 Proof.
-Induction 1; Auto.
+simple induction 1; auto.
 Qed.
 
-Inductive eq_dep1 [p:U;x:(P p);q:U;y:(P q)] : Prop :=
-   eq_dep1_intro : (h:q=p)
-                  (x=(eq_rect U q P y p h))->(eq_dep1 p x q y).
+Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
+    eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y.
 
 (** Invariance by Substitution of Reflexive Equality Proofs *)
 
-Axiom eq_rect_eq : (p:U)(Q:U->Type)(x:(Q p))(h:p=p)
-                  x=(eq_rect U p Q x p h).
+Axiom
+  eq_rect_eq :
+    forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
 
 Lemma eq_dep1_dep :
-      (p:U)(x:(P p))(q:U)(y:(P q))(eq_dep1 p x q y)->(eq_dep p x q y).
+ forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.
 Proof.
-Induction 1; Intros eq_qp.
-Cut (h:q=p)(y0:(P q))
-    (x=(eq_rect U q P y0 p h))->(eq_dep p x q y0).
-Intros; Apply H0 with eq_qp; Auto.
-Rewrite eq_qp; Intros h y0.
-Elim eq_rect_eq.
-Induction 1; Auto.
+simple induction 1; intros eq_qp.
+cut (forall (h:q = p) (y0:P q), x = eq_rect q P y0 p h -> eq_dep p x q y0).
+intros; apply H0 with eq_qp; auto.
+rewrite eq_qp; intros h y0.
+elim eq_rect_eq.
+simple induction 1; auto.
 Qed.
 
-Lemma eq_dep_dep1 : 
-  (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y).
+Lemma eq_dep_dep1 :
+ forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y.
 Proof.
-Induction 1; Intros.
-Apply eq_dep1_intro with (refl_equal U p).
-Simpl; Trivial.
+simple induction 1; intros.
+apply eq_dep1_intro with (refl_equal p).
+simpl in |- *; trivial.
 Qed.
 
-Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y.
+Lemma eq_dep1_eq : forall (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
 Proof.
-Induction 1; Intro.
-Elim eq_rect_eq; Auto.
+simple induction 1; intro.
+elim eq_rect_eq; auto.
 Qed.
 
 (** Injectivity of Dependent Equality is a consequence of *)
 (** Invariance by Substitution of Reflexive Equality Proof *)
 
-Lemma eq_dep_eq : (p:U)(x,y:(P p))(eq_dep p x p y)->x=y.
+Lemma eq_dep_eq : forall (p:U) (x y:P p), eq_dep p x p y -> x = y.
 Proof.
-Intros; Apply eq_dep1_eq; Apply eq_dep_dep1; Trivial.
+intros; apply eq_dep1_eq; apply eq_dep_dep1; trivial.
 Qed.
 
 End Dependent_Equality.
@@ -102,84 +103,88 @@ End Dependent_Equality.
 
 Scheme eq_indd := Induction for eq Sort Prop.
 
-Lemma UIP : (U:Type)(x,y:U)(p1,p2:x=y)p1=p2.
+Lemma UIP : forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2.
 Proof.
-Intros; Apply eq_dep_eq with P:=[y]x=y.
-Elim p2 using eq_indd.
-Elim p1 using eq_indd.
-Apply eq_dep_intro.
+intros; apply eq_dep_eq with (P := fun y => x = y).
+elim p2 using eq_indd.
+elim p1 using eq_indd.
+apply eq_dep_intro.
 Qed.
 
 (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
 
-Lemma UIP_refl : (U:Type)(x:U)(p:x=x)p=(refl_equal U x).
+Lemma UIP_refl : forall (U:Type) (x:U) (p:x = x), p = refl_equal x.
 Proof.
-Intros; Apply UIP.
+intros; apply UIP.
 Qed.
 
 (** Streicher axiom K is a direct consequence of Uniqueness of
     Reflexive Identity Proofs *)
 
-Lemma Streicher_K : (U:Type)(x:U)(P:x=x->Prop)
-  (P (refl_equal ? x))->(p:x=x)(P p).
+Lemma Streicher_K :
+ forall (U:Type) (x:U) (P:x = x -> Prop),
+   P (refl_equal x) -> forall p:x = x, P p.
 Proof.
-Intros; Rewrite UIP_refl; Assumption.
+intros; rewrite UIP_refl; assumption.
 Qed.
 
 (** We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *)
 
-Lemma eq_rec_eq : (U:Type)(P:U->Set)(p:U)(x:(P p))(h:p=p)
-  x=(eq_rec U p P x p h).
+Lemma eq_rec_eq :
+ forall (U:Type) (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.
 Proof.
-Intros.
-Apply Streicher_K with p:=h.
-Reflexivity.
+intros.
+apply Streicher_K with (p := h).
+reflexivity.
 Qed.
 
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
-Lemma equiv_eqex_eqdep : (U:Set)(P:U->Set)(p,q:U)(x:(P p))(y:(P q)) 
-    (existS U P p x)=(existS U P q y) <-> (eq_dep U P p x q y).
+Lemma equiv_eqex_eqdep :
+ forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
+   existS P p x = existS P q y <-> eq_dep U P p x q y.
 Proof.
-Split. 
+split. 
 (* -> *)
-Intro H.
-Change p with   (projS1 U P (existS U P p x)).
-Change 2 x with (projS2 U P (existS U P p x)).
-Rewrite H.
-Apply eq_dep_intro.
+intro H.
+change p with (projS1 (existS P p x)) in |- *.
+change x at 2 with (projS2 (existS P p x)) in |- *.
+rewrite H.
+apply eq_dep_intro.
 (* <- *)
-NewDestruct 1; Reflexivity.
+destruct 1; reflexivity.
 Qed.
 
 (** UIP implies the injectivity of equality on dependent pairs *)
 
-Lemma inj_pair2: (U:Set)(P:U->Set)(p:U)(x,y:(P p))
-    (existS U P p x)=(existS U P p y)-> x=y.
+Lemma inj_pair2 :
+ forall (U:Set) (P:U -> Set) (p:U) (x y:P p),
+   existS P p x = existS P p y -> x = y.
 Proof.
-Intros.
-Apply (eq_dep_eq U P).
-Generalize (equiv_eqex_eqdep U P p p x y) .
-Induction 1.
-Intros.
-Auto.
+intros.
+apply (eq_dep_eq U P).
+generalize (equiv_eqex_eqdep U P p p x y).
+simple induction 1.
+intros.
+auto.
 Qed.
 
 (** UIP implies the injectivity of equality on dependent pairs *)
 
-Lemma inj_pairT2: (U:Type)(P:U->Type)(p:U)(x,y:(P p))
-    (existT U P p x)=(existT U P p y)-> x=y.
+Lemma inj_pairT2 :
+ forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
+   existT P p x = existT P p y -> x = y.
 Proof.
-Intros.
-Apply (eq_dep_eq U P).
-Change 1 p with (projT1 U P (existT U P p x)).
-Change 2 x with (projT2 U P (existT U P p x)).
-Rewrite H.
-Apply eq_dep_intro.
+intros.
+apply (eq_dep_eq U P).
+change p at 1 with (projT1 (existT P p x)) in |- *.
+change x at 2 with (projT2 (existT P p x)) in |- *.
+rewrite H.
+apply eq_dep_intro.
 Qed.
 
 (** The main results to be exported *)
 
-Hints Resolve eq_dep_intro eq_dep_eq : core v62.
-Hints Immediate eq_dep_sym : core v62.
-Hints Resolve inj_pair2 inj_pairT2 : core.
+Hint Resolve eq_dep_intro eq_dep_eq: core v62.
+Hint Immediate eq_dep_sym: core v62.
+Hint Resolve inj_pair2 inj_pairT2: core.
\ No newline at end of file
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 8f7e76d51..22476505f 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -25,125 +25,134 @@
 Set Implicit Arguments.
 
   (** Bijection between [eq] and [eqT] *)
-  Definition eq2eqT: (A:Set)(x,y:A)x=y->x==y :=
-    [A,x,_,eqxy]<[y:A]x==y>Cases eqxy of refl_equal => (refl_eqT ? x) end.
-
-  Definition eqT2eq: (A:Set)(x,y:A)x==y->x=y :=
-    [A,x,_,eqTxy]<[y:A]x=y>Cases eqTxy of refl_eqT => (refl_equal ? x) end.
-
-  Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)).
-Intros.
-Case p; Reflexivity.
+  Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) : 
+    x = y :=
+    match eqxy in (_ = y) return x = y with
+    | refl_equal => refl_equal x
+    end.
+
+  Definition eqT2eq (A:Set) (x y:A) (eqTxy:x = y) : 
+    x = y :=
+    match eqTxy in (_ = y) return x = y with
+    | refl_equal => refl_equal x
+    end.
+
+  Lemma eq_eqT_bij : forall (A:Set) (x y:A) (p:x = y), p = eqT2eq (eq2eqT p).
+intros.
+case p; reflexivity.
 Qed.
 
-  Lemma eqT_eq_bij: (A:Set)(x,y:A)(p:x==y)p==(eq2eqT (eqT2eq p)).
-Intros.
-Case p; Reflexivity.
+  Lemma eqT_eq_bij : forall (A:Set) (x y:A) (p:x = y), p = eq2eqT (eqT2eq p).
+intros.
+case p; reflexivity.
 Qed.
 
 
 Section DecidableEqDep.
 
-  Variable A: Type.
+  Variable A : Type.
 
-  Local comp [x,y,y':A]: x==y->x==y'->y==y' :=
-    [eq1,eq2](eqT_ind ? ? [a]a==y' eq2 ? eq1).
+  Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
+    eq_ind _ (fun a => a = y') eq2 _ eq1.
 
-  Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y).
-Intros.
-Case u; Trivial.
+  Remark trans_sym_eqT : forall (x y:A) (u:x = y), comp u u = refl_equal y.
+intros.
+case u; trivial.
 Qed.
 
 
 
-  Variable eq_dec: (x,y:A) x==y \/ ~x==y.
+  Variable eq_dec : forall x y:A, x = y \/ x <> y.
 
-  Variable x: A.
+  Variable x : A.
 
 
-  Local nu [y:A]: x==y->x==y :=
-    [u]Cases (eq_dec x y) of
-       (or_introl eqxy)  => eqxy
-     | (or_intror neqxy) => (False_ind ? (neqxy u))
-     end.
+  Let nu (y:A) (u:x = y) : x = y :=
+    match eq_dec x y with
+    | or_introl eqxy => eqxy
+    | or_intror neqxy => False_ind _ (neqxy u)
+    end.
 
-  Local nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v).
-Intros.
-Unfold nu.
-Case (eq_dec x y); Intros.
-Reflexivity.
+  Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
+intros.
+unfold nu in |- *.
+case (eq_dec x y); intros.
+reflexivity.
 
-Case n; Trivial.
+case n; trivial.
 Qed.
 
 
-  Local nu_inv [y:A]: x==y->x==y := [v](comp (nu (refl_eqT ? x)) v).
+  Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v.
 
 
-  Remark nu_left_inv : (y:A)(u:x==y) (nu_inv (nu u))==u.
-Intros.
-Case u; Unfold nu_inv.
-Apply trans_sym_eqT.
+  Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
+intros.
+case u; unfold nu_inv in |- *.
+apply trans_sym_eqT.
 Qed.
 
 
-  Theorem eq_proofs_unicity: (y:A)(p1,p2:x==y) p1==p2.
-Intros.
-Elim nu_left_inv with u:=p1.
-Elim nu_left_inv with u:=p2.
-Elim nu_constant with y p1 p2.
-Reflexivity.
+  Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
+intros.
+elim nu_left_inv with (u := p1).
+elim nu_left_inv with (u := p2).
+elim nu_constant with y p1 p2.
+reflexivity.
 Qed.
 
-  Theorem K_dec: (P:x==x->Prop)(P (refl_eqT ? x)) -> (p:x==x)(P p).
-Intros.
-Elim eq_proofs_unicity with x (refl_eqT ? x) p.
-Trivial.
+  Theorem K_dec :
+   forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.
+intros.
+elim eq_proofs_unicity with x (refl_equal x) p.
+trivial.
 Qed.
 
 
   (** The corollary *)
 
-  Local proj: (P:A->Prop)(ExT P)->(P x)->(P x) :=
-    [P,exP,def]Cases exP of
-      (exT_intro x' prf) =>
-        Cases (eq_dec x' x) of
-          (or_introl eqprf) => (eqT_ind ? x' P prf x eqprf)
+  Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
+    match exP with
+    | ex_intro x' prf =>
+        match eq_dec x' x with
+        | or_introl eqprf => eq_ind x' P prf x eqprf
         | _ => def
         end
-      end.
+    end.
 
 
-  Theorem inj_right_pair: (P:A->Prop)(y,y':(P x))
-    (exT_intro ? P x y)==(exT_intro ? P x y') -> y==y'.
-Intros.
-Cut (proj (exT_intro A P x y) y)==(proj (exT_intro A P x y') y).
-Simpl.
-Case (eq_dec x x).
-Intro e.
-Elim e using K_dec; Trivial.
+  Theorem inj_right_pair :
+   forall (P:A -> Prop) (y y':P x),
+     ex_intro P x y = ex_intro P x y' -> y = y'.
+intros.
+cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
+simpl in |- *.
+case (eq_dec x x).
+intro e.
+elim e using K_dec; trivial.
 
-Intros.
-Case n; Trivial.
+intros.
+case n; trivial.
 
-Case H.
-Reflexivity.
+case H.
+reflexivity.
 Qed.
 
 End DecidableEqDep.
 
   (** We deduce the [K] axiom for (decidable) Set *)
-  Theorem K_dec_set: (A:Set)((x,y:A){x=y}+{~x=y})
-                       ->(x:A)(P: x=x->Prop)(P (refl_equal ? x))
-                         ->(p:x=x)(P p).
-Intros.
-Rewrite eq_eqT_bij.
-Elim (eq2eqT p) using K_dec.
-Intros.
-Case (H x0 y); Intros.
-Elim e; Left ; Reflexivity.
-
-Right ; Red; Intro neq; Apply n; Elim neq; Reflexivity.
-
-Trivial.
-Qed.
+  Theorem K_dec_set :
+   forall A:Set,
+     (forall x y:A, {x = y} + {x <> y}) ->
+     forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+intros.
+rewrite eq_eqT_bij.
+elim (eq2eqT p) using K_dec.
+intros.
+case (H x0 y); intros.
+elim e; left; reflexivity.
+
+right; red in |- *; intro neq; apply n; elim neq; reflexivity.
+
+trivial.
+Qed.
\ No newline at end of file
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 44d259431..8ae8a545f 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -31,53 +31,55 @@ Section Paradox.
 Variable bool : Prop.
 Variable p2b : Prop -> bool.
 Variable b2p : bool -> Prop.
-Hypothesis p2p1 : (A:Prop)(b2p (p2b A))->A.
-Hypothesis p2p2 : (A:Prop)A->(b2p (p2b A)).
-Variable B:Prop.
+Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
+Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
+Variable B : Prop.
 
-Definition V := (A:Prop)((A->bool)->(A->bool))->(A->bool).
-Definition U := V->bool.
-Definition sb : V -> V := [z][A;r;a](r (z A r) a).
-Definition le : (U->bool)->(U->bool) := [i][x](x [A;r;a](i [v](sb v A r a))).
-Definition induct : (U->bool)->Prop := [i](x:U)(b2p (le i x))->(b2p (i x)).
-Definition WF : U := [z](p2b (induct (z U le))).
-Definition I : U->Prop :=
-  [x]((i:U->bool)(b2p (le i x))->(b2p (i [v](sb v U le x))))->B.
+Definition V := forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool.
+Definition U := V -> bool.
+Definition sb (z:V) : V := fun A r a => r (z A r) a.
+Definition le (i:U -> bool) (x:U) : bool :=
+  x (fun A r a => i (fun v => sb v A r a)).
+Definition induct (i:U -> bool) : Prop :=
+  forall x:U, b2p (le i x) -> b2p (i x).
+Definition WF : U := fun z => p2b (induct (z U le)).
+Definition I (x:U) : Prop :=
+  (forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B.
 
-Lemma Omega : (i:U->bool)(induct i)->(b2p (i WF)).
+Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF).
 Proof.
-Intros i y.
-Apply y.
-Unfold le WF induct.
-Apply p2p2.
-Intros x H0.
-Apply y.
-Exact H0.
+intros i y.
+apply y.
+unfold le, WF, induct in |- *.
+apply p2p2.
+intros x H0.
+apply y.
+exact H0.
 Qed.
 
-Lemma lemma1 : (induct [u](p2b (I u))).
+Lemma lemma1 : induct (fun u => p2b (I u)).
 Proof.
-Unfold induct.
-Intros x p.
-Apply (p2p2 (I x)).
-Intro q.
-Apply (p2p1 (I [v:V](sb v U le x)) (q [u](p2b (I u)) p)).
-Intro i.
-Apply q with i:=[y:?](i [v:V](sb v U le y)).
+unfold induct in |- *.
+intros x p.
+apply (p2p2 (I x)).
+intro q.
+apply (p2p1 (I (fun v:V => sb v U le x)) (q (fun u => p2b (I u)) p)).
+intro i.
+apply q with (i := fun y => i (fun v:V => sb v U le y)).
 Qed.
 
-Lemma lemma2 : ((i:U->bool)(induct i)->(b2p (i WF)))->B.
+Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B.
 Proof.
-Intro x.
-Apply (p2p1 (I WF) (x [u](p2b (I u)) lemma1)).
-Intros i H0.
-Apply (x [y](i [v](sb v U le y))).
-Apply (p2p1 ? H0).
+intro x.
+apply (p2p1 (I WF) (x (fun u => p2b (I u)) lemma1)).
+intros i H0.
+apply (x (fun y => i (fun v => sb v U le y))).
+apply (p2p1 _ H0).
 Qed.
 
 Theorem paradox : B.
 Proof.
-Exact (lemma2 Omega).
+exact (lemma2 Omega).
 Qed.
 
-End Paradox.
+End Paradox.
\ No newline at end of file
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 04c62b3a1..10c9083f0 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -12,53 +12,57 @@
 
 Set Implicit Arguments.
 
-Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := 
-	JMeq_refl : (JMeq x x).
+Inductive JMeq (A:Set) (x:A) : forall B:Set, B -> Prop :=
+    JMeq_refl : JMeq x x.
 Reset JMeq_ind.
 
-Hints Resolve JMeq_refl.
+Hint Resolve JMeq_refl.
 
-Lemma sym_JMeq : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
-NewDestruct 1; Trivial.
+Lemma sym_JMeq : forall (A B:Set) (x:A) (y:B), JMeq x y -> JMeq y x.
+destruct 1; trivial.
 Qed.
 
-Hints Immediate sym_JMeq.
+Hint Immediate sym_JMeq.
 
-Lemma trans_JMeq : (A,B,C:Set)(x:A)(y:B)(z:C)
-	(JMeq x y)->(JMeq y z)->(JMeq x z).
-NewDestruct 1; Trivial.
+Lemma trans_JMeq :
+ forall (A B C:Set) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
+destruct 1; trivial.
 Qed.
 
-Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y).
+Axiom JMeq_eq : forall (A:Set) (x y:A), JMeq x y -> x = y.
 
-Lemma JMeq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y).
-Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
+Lemma JMeq_ind : forall (A:Set) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
+intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y).
-Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
+Lemma JMeq_rec : forall (A:Set) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
+intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x).
-Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial.
+Lemma JMeq_ind_r :
+ forall (A:Set) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
+intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
-Lemma JMeq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x).
-Intros A x y P H H'; Case JMeq_eq with 1:=(sym_JMeq H'); Trivial.
+Lemma JMeq_rec_r :
+ forall (A:Set) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
+intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
 (** [JMeq] is equivalent to [(eq_dep Set [X]X)] *)
 
-Require Eqdep.
+Require Import Eqdep.
 
-Lemma JMeq_eq_dep : (A,B:Set)(x:A)(y:B)(JMeq x y)->(eq_dep Set [X]X A x B y).
+Lemma JMeq_eq_dep :
+ forall (A B:Set) (x:A) (y:B), JMeq x y -> eq_dep Set (fun X => X) A x B y.
 Proof.
-NewDestruct 1.
-Apply eq_dep_intro.
+destruct 1.
+apply eq_dep_intro.
 Qed.
 
-Lemma eq_dep_JMeq : (A,B:Set)(x:A)(y:B)(eq_dep Set [X]X A x B y)->(JMeq x y).
+Lemma eq_dep_JMeq :
+ forall (A B:Set) (x:A) (y:B), eq_dep Set (fun X => X) A x B y -> JMeq x y.
 Proof.
-NewDestruct 1.
-Apply JMeq_refl. 
-Qed.
+destruct 1.
+apply JMeq_refl. 
+Qed.
\ No newline at end of file
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index ab2ca17c2..8636e5ddc 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -30,57 +30,62 @@
     paradox of system U- (e.g. Hurkens' paradox).
 *)
 
-Require Hurkens.
+Require Import Hurkens.
 
 Section Proof_irrelevance_CC.
 
 Variable or : Prop -> Prop -> Prop.
-Variable or_introl : (A,B:Prop)A->(or A B).
-Variable or_intror : (A,B:Prop)B->(or A B).
-Hypothesis or_elim : (A,B:Prop)(C:Prop)(A->C)->(B->C)->(or A B)->C.
-Hypothesis or_elim_redl :
-  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(a:A)
-  (f a)==(or_elim A B C f g (or_introl A B a)).
-Hypothesis or_elim_redr :
-  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(b:B)
-  (g b)==(or_elim A B C f g (or_intror A B b)).
-Hypothesis or_dep_elim :
- (A,B:Prop)(P:(or A B)->Prop)
- ((a:A)(P (or_introl A B a))) ->
- ((b:B)(P (or_intror A B b))) -> (b:(or A B))(P b).
-
-Hypothesis em : (A:Prop)(or A ~A).
+Variable or_introl : forall A B:Prop, A -> or A B.
+Variable or_intror : forall A B:Prop, B -> or A B.
+Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
+Hypothesis
+  or_elim_redl :
+    forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
+      f a = or_elim A B C f g (or_introl A B a).
+Hypothesis
+  or_elim_redr :
+    forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
+      g b = or_elim A B C f g (or_intror A B b).
+Hypothesis
+  or_dep_elim :
+    forall (A B:Prop) (P:or A B -> Prop),
+      (forall a:A, P (or_introl A B a)) ->
+      (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.
+
+Hypothesis em : forall A:Prop, or A (~ A).
 Variable B : Prop.
-Variable b1,b2 : B.
+Variables b1 b2 : B.
 
 (** [p2b] and [b2p] form a retract if [~b1==b2] *)
 
-Definition p2b [A] := (or_elim A ~A B [_]b1 [_]b2 (em A)).
-Definition b2p [b] := b1==b.
+Definition p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
+Definition b2p b := b1 = b.
 
-Lemma p2p1 : (A:Prop) A -> (b2p (p2b A)).
+Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
 Proof.
-  Unfold p2b; Intro A; Apply or_dep_elim with b:=(em A); Unfold b2p; Intros.
-  Apply (or_elim_redl A ~A B [_]b1 [_]b2).
-  NewDestruct (b H).
+  unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
+   unfold b2p in |- *; intros.
+  apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).
+  destruct (b H).
 Qed.
-Lemma p2p2 :  ~b1==b2->(A:Prop) (b2p (p2b A)) -> A.
+Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.
 Proof.
-  Intro not_eq_b1_b2.
-  Unfold p2b; Intro A; Apply or_dep_elim with b:=(em A); Unfold b2p; Intros.
-  Assumption.
-  NewDestruct not_eq_b1_b2.
-  Rewrite <- (or_elim_redr A ~A B [_]b1 [_]b2) in H.
-  Assumption.
+  intro not_eq_b1_b2.
+  unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
+   unfold b2p in |- *; intros.
+  assumption.
+  destruct not_eq_b1_b2.
+  rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.
+  assumption.
 Qed.
 
 (** Using excluded-middle a second time, we get proof-irrelevance *)
 
-Theorem proof_irrelevance_cc : b1==b2.
+Theorem proof_irrelevance_cc : b1 = b2.
 Proof.
-  Refine (or_elim ? ? ? ? ? (em b1==b2));Intro H.
-    Trivial.
-  Apply (paradox B p2b b2p (p2p2 H) p2p1).
+  refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.
+    trivial.
+  apply (paradox B p2b b2p (p2p2 H) p2p1).
 Qed.
 
 End Proof_irrelevance_CC.
@@ -92,26 +97,22 @@ End Proof_irrelevance_CC.
 
 Section Proof_irrelevance_CCI.
 
-Hypothesis em : (A:Prop) A \/ ~A.
+Hypothesis em : forall A:Prop, A \/ ~ A.
 
-Definition or_elim_redl :
-  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(a:A)
-  (f a)==(or_ind A B C f g (or_introl A B a))
-  := [A,B,C;f;g;a](refl_eqT C (f a)).
-Definition or_elim_redr :
-  (A,B:Prop)(C:Prop)(f:A->C)(g:B->C)(b:B)
-  (g b)==(or_ind A B C f g (or_intror A B b))
-  := [A,B,C;f;g;b](refl_eqT C (g b)).
+Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C) 
+  (a:A) : f a = or_ind f g (or_introl B a) := refl_equal (f a).
+Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C) 
+  (b:B) : g b = or_ind f g (or_intror A b) := refl_equal (g b).
 Scheme or_indd := Induction for or Sort Prop.
 
-Theorem proof_irrelevance_cci : (B:Prop)(b1,b2:B)b1==b2.
+Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.
 Proof
-  (proof_irrelevance_cc or or_introl or_intror or_ind
-     or_elim_redl or_elim_redr or_indd em).
+  proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
+    or_elim_redr or_indd em.
 
 End Proof_irrelevance_CCI.
 
 (** Remark: in CCI, [bool] can be taken in [Set] as well in the
     paradox and since [~true=false] for [true] and [false] in
     [bool], we get the inconsistency of [em : (A:Prop){A}+{~A}] in CCI
-*)
+*)
\ No newline at end of file
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 5addb4d24..c55095e47 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -10,8 +10,11 @@
 
 (* This file axiomatizes the relational form of the axiom of choice *)
 
-Axiom relational_choice :
- (A:Type;B:Type;R: A->B->Prop) 
-  ((x:A)(EX y:B|(R x y)))
-   -> (EXT R':A->B->Prop | 
-         ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))).
+Axiom
+  relational_choice :
+    forall (A B:Type) (R:A -> B -> Prop),
+      (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')).
\ No newline at end of file