Mise en forme des theories

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

1 files changed, 32 insertions, 31 deletions

diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 0c4c8399c..265851ec7 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -17,39 +17,40 @@ Definition Qeq_bool (x y : Q) :=
   if Qeq_dec x y then true else false.
 
 Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
-intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
-intros _ H; inversion H.
+Proof.
+  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
+  intros _ H; inversion H.
 Qed.
 
 Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
 Proof.
-constructor.
-exact Qplus_0_l.
-exact Qplus_comm.
-exact Qplus_assoc.
-exact Qmult_1_l.
-exact Qmult_comm.
-exact Qmult_assoc.
-exact Qmult_plus_distr_l.
-reflexivity.
-exact Qplus_opp_r.
+  constructor.
+  exact Qplus_0_l.
+  exact Qplus_comm.
+  exact Qplus_assoc.
+  exact Qmult_1_l.
+  exact Qmult_comm.
+  exact Qmult_assoc.
+  exact Qmult_plus_distr_l.
+  reflexivity.
+  exact Qplus_opp_r.
 Qed.
 
 Ltac isQcst t :=
   let t := eval hnf in t in
-  match t with
-    Qmake ?n ?d =>
+    match t with
+      Qmake ?n ?d =>
       match isZcst n with
         true => isZcst d
-      | _ => false
+	| _ => false
       end
-  | _ => false
-  end.
+      | _ => false
+    end.
 
 Ltac Qcst t :=
   match isQcst t with
     true => t
-  | _ => NotConstant
+    | _ => NotConstant
   end.
 
 Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
@@ -58,46 +59,46 @@ Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
 Section Examples. 
 
 Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
-intros.
-ring.
+  intros.
+  ring.
 Qed.
 
 Let ex2 : forall x y : Q, x+y == y+x.
-intros. 
-ring.
+  intros. 
+  ring.
 Qed.
 
 Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
-intros.
-ring.
+  intros.
+  ring.
 Qed.
 
 Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
-ring.
+  ring.
 Qed.
 
 Let ex5 : 1+1 == 2#1.
-ring.
+  ring.
 Qed.
 
 Let ex6 : (1#1)+(1#1) == 2#1.
-ring.
+  ring.
 Qed.
 
 Let ex7 : forall x : Q, x-x== 0#1.
-intro.
-ring.
+  intro.
+  ring.
 Qed.
 
 End Examples.
 
 Lemma Qopp_plus : forall a b,  -(a+b) == -a + -b.
 Proof.
-intros; ring.
+  intros; ring.
 Qed.
 
 Lemma Qopp_opp : forall q, - -q==q.
 Proof.
-intros; ring.
+  intros; ring.
 Qed.