1 files changed, 31 insertions, 30 deletions

diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index 61204ba30..ef48e6272 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -20,53 +20,54 @@ Section Bool_eq_dec.
 
   Variable beq : A -> A -> bool.
 
-  Variable beq_refl : (x:A)true=(beq x x).
+  Variable beq_refl : forall x:A, true = beq x x.
 
-  Variable beq_eq : (x,y:A)true=(beq x y)->x=y.
+  Variable beq_eq : forall x y:A, true = beq x y -> x = y.
 
-  Definition beq_eq_true : (x,y:A)x=y->true=(beq x y).
+  Definition beq_eq_true : forall x y:A, x = y -> true = beq x y.
   Proof.
-    Intros x y H.
-    Case H.
-    Apply beq_refl.
+    intros x y H.
+    case H.
+    apply beq_refl.
   Defined.
 
-  Definition beq_eq_not_false : (x,y:A)x=y->~false=(beq x y).
+  Definition beq_eq_not_false : forall x y:A, x = y -> false <> beq x y.
   Proof.
-    Intros x y e.
-    Rewrite <- beq_eq_true; Trivial; Discriminate.
+    intros x y e.
+    rewrite <- beq_eq_true; trivial; discriminate.
   Defined.
 
-  Definition beq_false_not_eq : (x,y:A)false=(beq x y)->~x=y.
+  Definition beq_false_not_eq : forall x y:A, false = beq x y -> x <> y.
   Proof.
-    Exact [x,y:A; H:(false=(beq x y)); e:(x=y)](beq_eq_not_false x y e H).
+    exact
+     (fun (x y:A) (H:false = beq x y) (e:x = y) => beq_eq_not_false x y e H).
   Defined.
 
-  Definition exists_beq_eq : (x,y:A){b:bool | b=(beq x y)}.
+  Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
   Proof.
-    Intros.
-    Exists (beq x y).
-    Constructor.
+    intros.
+    exists (beq x y).
+    constructor.
   Defined.
 
-  Definition not_eq_false_beq : (x,y:A)~x=y->false=(beq x y).
+  Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y.
   Proof.
-    Intros x y H.
-    Symmetry.
-    Apply not_true_is_false.
-    Intro.
-    Apply H.
-    Apply beq_eq.
-    Symmetry.
-    Assumption.
+    intros x y H.
+    symmetry  in |- *.
+    apply not_true_is_false.
+    intro.
+    apply H.
+    apply beq_eq.
+    symmetry  in |- *.
+    assumption.
   Defined.
 
-  Definition eq_dec : (x,y:A){x=y}+{~x=y}.
+  Definition eq_dec : forall x y:A, {x = y} + {x <> y}.
   Proof.
-    Intros x y; Case (exists_beq_eq x y).
-    Intros b; Case b; Intro H.
-      Left; Apply beq_eq; Assumption.
-      Right; Apply beq_false_not_eq; Assumption.
+    intros x y; case (exists_beq_eq x y).
+    intros b; case b; intro H.
+      left; apply beq_eq; assumption.
+      right; apply beq_false_not_eq; assumption.
   Defined.
 
-End Bool_eq_dec.
+End Bool_eq_dec.
\ No newline at end of file