From d857c99c6c985eb36ce8a4b2667dc0b5ccca115c Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 20 Apr 2001 16:00:43 +0000
Subject: Library doc adjustments (until page 140)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1655 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/IntMap/Addec.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'theories/IntMap/Addec.v')

diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index abbe450816..72ad3d9866 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -73,7 +73,8 @@ Proof.
   Intros. Rewrite (ad_xor_eq a a' H). Apply ad_eq_correct.
 Qed.
 
-Lemma ad_xor_eq_false : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false.
+Lemma ad_xor_eq_false 
+  : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false.
 Proof.
   Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0.
   Rewrite (ad_eq_complete a a' H0) in H. Rewrite (ad_xor_nilpotent a') in H. Discriminate H.
@@ -115,14 +116,16 @@ Proof.
   Intro H0. Rewrite ad_eq_comm. Assumption.
 Qed.
 
-Lemma ad_bit_0_neq : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false.
+Lemma ad_bit_0_neq 
+  : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false.
 Proof.
   Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H1. Rewrite (ad_eq_complete ? ? H1) in H.
   Rewrite H in H0. Discriminate H0.
   Trivial.
 Qed.
 
-Lemma ad_div_eq : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true.
+Lemma ad_div_eq 
+  : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true.
 Proof.
   Intros. Cut a=a'. Intros. Rewrite H0. Apply ad_eq_correct.
   Apply ad_eq_complete. Exact H.
-- 
cgit v1.2.3