Add some missing Proof statements.

11 files changed, 24 insertions, 4 deletions

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d82fa602a..c483b1d83 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -32,8 +32,7 @@ Section Well_founded.
   (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
   (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)
 
-  Hypothesis
-    F_ext :
+  Hypothesis F_ext :
     forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
       (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
 
@@ -63,6 +62,7 @@ Section Well_founded.
       Fix_sub x =
       let f_sub := F_sub in
         f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)).
+  Proof.
     exact Fix_eq.
   Qed.
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 2ed7a29ea..fb7f4c4a4 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -520,6 +520,7 @@ Add Field Qcfield : Qcft.
 (** A field tactic for rational numbers *)
 
 Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc.
+Proof.
 intros.
 field.
 auto.
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 5d494c7c8..db77567a7 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -41,6 +41,7 @@ try destruct (Qmult_integral _ _ H0); auto.
 Qed.
 
 Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n.
+Proof.
 intros p n Hp.
 induction n; simpl; repeat apply Qmult_le_0_compat;assumption.
 Qed.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index f363fd7c2..8f827dab9 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -14,6 +14,7 @@ Require Export QArith_base.
 Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
 
 Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.
+Proof.
 intros; apply not_O_IZR; auto with qarith.
 Qed.
 
@@ -162,6 +163,7 @@ field; auto.
 Qed.
 
 Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R.
+Proof.
 unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto.
 Qed.
 
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 3b3a30eb9..2aac617eb 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -126,11 +126,13 @@ Proof.
 Qed.
 
 Add Morphism Qmult' : Qmult'_comp.
+Proof.
   intros; unfold Qmult'.
   rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qminus' : Qminus'_comp.
+Proof.
   intros; unfold Qminus'.
   rewrite H, H0; auto with qarith.
 Qed.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 1ec399d19..3c738e984 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -11,16 +11,19 @@ Require Import Omega.
 Local Open Scope R_scope.
 
 Lemma Rlt_R0_R2 : 0 < 2.
+Proof.
 change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
 Qed.
 
 Notation Rplus_lt_pos := Rplus_lt_0_compat (only parsing).
 
 Lemma IZR_eq : forall z1 z2:Z, z1 = z2 -> IZR z1 = IZR z2.
+Proof.
 intros; rewrite H; reflexivity.
 Qed.
 
 Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
+Proof.
 intros; red; intro; elim H; apply eq_IZR; assumption.
 Qed.
 
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 311f29098..cfb50231c 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -28,6 +28,7 @@ Lemma atan_sub_correct :
  forall u v, 1 + u * v <> 0 -> -PI/2 < atan u - atan v < PI/2 ->
    -PI/2 < atan (atan_sub u v) < PI/2 ->
    atan u = atan v + atan (atan_sub u v).
+Proof.
 intros u v pn0 uvint aint.
 assert (cos (atan u) <> 0).
  destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto.
@@ -45,6 +46,7 @@ Qed.
 
 Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> 
   -PI/2 < atan x - atan y < PI/2.
+Proof.
 assert (ut := PI_RGT_0).
 intros x y [xm1 x1] [ym1 y1].
 assert (-(PI/4) <= atan x).
@@ -68,6 +70,7 @@ Qed.
 
 (* A simple formula, reasonably efficient. *)
 Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3).
+Proof.
 assert (utility : 0 < PI/2) by (apply PI2_RGT_0).
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/2)).
@@ -78,6 +81,7 @@ apply atan_bound.
 Qed.
 
 Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239).
+Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/5));
  [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
@@ -106,6 +110,7 @@ unfold atan_sub; field.
 Qed.
 
 Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)).
+Proof.
 rewrite <- atan_1.
 rewrite (atan_sub_correct 1 (/3));
  [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier |
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index f3e690376..76d52efaa 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -221,6 +221,7 @@ Proof.
 Qed.
 
 Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.
+Proof.
   intro; unfold cos_n; unfold Rdiv; apply prod_neq_R0.
   apply pow_nonzero; discrR.
   apply Rinv_neq_0_compat.
@@ -233,6 +234,7 @@ Definition cos_in (x l:R) : Prop :=
 
 (**********)
 Lemma exist_cos : forall x:R, { l:R | cos_in x l }.
+Proof.
   intro; generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos).
   unfold Pser, cos_in; trivial.
 Qed.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index eec7aa2d7..2ffe70bff 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -16,14 +16,17 @@ Definition Setoid_Theory := @Equivalence.
 Definition Build_Setoid_Theory := @Build_Equivalence.
 
 Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
+Proof.
   unfold Setoid_Theory in s. intros ; reflexivity.
 Defined.
 
 Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x.
+Proof.
   unfold Setoid_Theory in s. intros ; symmetry ; assumption.
 Defined.
 
 Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z.
+Proof.
   unfold Setoid_Theory in s. intros ; transitivity y ; assumption.
 Defined.
 
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 7d7dcc6d0..746161b38 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -34,6 +34,7 @@ Definition shift (c : bool) (a : ascii) :=
 (** Definition of a decidable function that is effective *)
 
 Definition ascii_dec : forall a b : ascii, {a = b} + {a <> b}.
+Proof.
   decide equality; apply bool_dec.
 Defined.
 
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 6294d156b..1479695d8 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -29,6 +29,7 @@ Local Open Scope string_scope.
 (** Equality is decidable *)
 
 Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.
+Proof.
  decide equality; apply ascii_dec.
 Defined.
 
@@ -41,7 +42,6 @@ Fixpoint append (s1 s2 : string) : string :=
   | EmptyString => s2
   | String c s1' => String c (s1' ++ s2)
   end
-
 where "s1 ++ s2" := (append s1 s2) : string_scope.
 
 (******************************)
@@ -379,7 +379,7 @@ Definition findex n s1 s2 :=
 (**
   The concrete syntax for strings in scope string_scope follows the
   Coq convention for strings: all ascii characters of code less than
-  128 are litteral to the exception of the character `double quote'
+  128 are literals to the exception of the character `double quote'
   which must be doubled.
 
   Strings that involve ascii characters of code >= 128 which are not