1 files changed, 34 insertions, 34 deletions
diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v
index 364cc8d6a4..6563fb68ac 100644
--- a/contrib/correctness/ProgBool.v
+++ b/contrib/correctness/ProgBool.v
@@ -10,57 +10,57 @@
 
 (* $Id$ *)
 
-Require ZArith.
+Require Import ZArith.
 Require Export Bool_nat.
 Require Export Sumbool.
 
 Definition annot_bool :
-  (b:bool) { b':bool | if b' then b=true else b=false }.
+  forall b:bool, {b' : bool | if b' then b = true else b = false}.
 Proof.
-Intro b.
-Exists b. Case b; Trivial.
-Save.
+intro b.
+exists b. case b; trivial.
+Qed.
 
 
 (* Logical connectives *)
 
-Definition spec_and := [A,B,C,D:Prop][b:bool]if b then A /\ C else B \/ D.
+Definition spec_and (A B C D:Prop) (b:bool) := if b then A /\ C else B \/ D.
 
 Definition prog_bool_and :
-  (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool Q2)
-  -> { b:bool | if b then (Q1 true) /\ (Q2 true)
-                     else (Q1 false) \/ (Q2 false) }.
+  forall Q1 Q2:bool -> Prop,
+    sig Q1 ->
+    sig Q2 ->
+    {b : bool | if b then Q1 true /\ Q2 true else Q1 false \/ Q2 false}.
 Proof.
-Intros Q1 Q2 H1 H2.
-Elim H1. Intro b1. Elim H2. Intro b2. 
-Case b1; Case b2; Intros.
-Exists true; Auto.
-Exists false; Auto. Exists false; Auto. Exists false; Auto.
-Save.
+intros Q1 Q2 H1 H2.
+elim H1. intro b1. elim H2. intro b2. 
+case b1; case b2; intros.
+exists true; auto.
+exists false; auto. exists false; auto. exists false; auto.
+Qed.
 
-Definition spec_or := [A,B,C,D:Prop][b:bool]if b then A \/ C else B /\ D.
+Definition spec_or (A B C D:Prop) (b:bool) := if b then A \/ C else B /\ D.
 
 Definition prog_bool_or :
-  (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool Q2)
-  -> { b:bool | if b then (Q1 true) \/ (Q2 true)
-                     else (Q1 false) /\ (Q2 false) }.
+  forall Q1 Q2:bool -> Prop,
+    sig Q1 ->
+    sig Q2 ->
+    {b : bool | if b then Q1 true \/ Q2 true else Q1 false /\ Q2 false}.
 Proof.
-Intros Q1 Q2 H1 H2.
-Elim H1. Intro b1. Elim H2. Intro b2. 
-Case b1; Case b2; Intros.
-Exists true; Auto. Exists true; Auto. Exists true; Auto.
-Exists false; Auto.
-Save.
+intros Q1 Q2 H1 H2.
+elim H1. intro b1. elim H2. intro b2. 
+case b1; case b2; intros.
+exists true; auto. exists true; auto. exists true; auto.
+exists false; auto.
+Qed.
 
-Definition spec_not:= [A,B:Prop][b:bool]if b then B else A.
+Definition spec_not (A B:Prop) (b:bool) := if b then B else A.
 
 Definition prog_bool_not :
-  (Q:bool->Prop) (sig bool Q)
-  -> { b:bool | if b then (Q false) else (Q true) }.
+  forall Q:bool -> Prop, sig Q -> {b : bool | if b then Q false else Q true}.
 Proof.
-Intros Q H.
-Elim H. Intro b.
-Case b; Intro.
-Exists false; Auto. Exists true; Auto.
-Save.
-
+intros Q H.
+elim H. intro b.
+case b; intro.
+exists false; auto. exists true; auto.
+Qed.