Add some missing Proof statements.

4 files changed, 6 insertions, 0 deletions

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.