Nettoyages pour doc

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1471 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 14 insertions, 20 deletions

diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 4f4123e..f183ade 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -320,18 +320,12 @@ End EXPR.
 
 Inductive cont: Type :=
   | Kstop: cont
-  | Kseq: statement -> cont -> cont
-       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
-  | Kwhile: expr -> statement -> cont -> cont
-       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
-  | Kdowhile: expr -> statement -> cont -> cont
-       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
-  | Kfor2: expr -> statement -> statement -> cont -> cont
-       (**r [Kfor2 e2 e3 s k] = after [s] in [for'(e2;e3) s] *)
-  | Kfor3: expr -> statement -> statement -> cont -> cont
-       (**r [Kfor3 e2 e3 s k] = after [e3] in [for'(e2;e3) s] *)
-  | Kswitch: cont -> cont
-       (**r catches [break] statements arising out of [switch] *)
+  | Kseq: statement -> cont -> cont       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
+  | Kwhile: expr -> statement -> cont -> cont       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
+  | Kdowhile: expr -> statement -> cont -> cont       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
+  | Kfor2: expr -> statement -> statement -> cont -> cont       (**r [Kfor2 e2 e3 s k] = after [s] in [for'(e2;e3) s] *)
+  | Kfor3: expr -> statement -> statement -> cont -> cont       (**r [Kfor3 e2 e3 s k] = after [e3] in [for'(e2;e3) s] *)
+  | Kswitch: cont -> cont       (**r catches [break] statements arising out of [switch] *)
   | Kcall: option ident ->                  (**r where to store result *)
            function ->                      (**r calling function *)
            env ->                           (**r local env of calling function *)
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 3f29915..742a969 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -213,13 +213,13 @@ Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   | add_case_pi ty =>                   (**r pointer plus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 => 
-	Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
       | _,  _ => None
       end   
   | add_case_ip ty =>                   (**r integer plus pointer *)
       match v1,v2 with
       | Vint n1, Vptr b2 ofs2 => 
-	Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
+        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
       | _,  _ => None
       end   
   | add_default => None
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index ad99162..fc97945 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -221,7 +221,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       match r with Eval _ _ => False | _ => True end ->
       ty = typeof r ->
       estep (ExprState f r k e m)
-	 E0 (ExprState f (Eval v ty) k e m)
+         E0 (ExprState f (Eval v ty) k e m)
 
   | step_condition_true: forall f C r1 r2 r3 ty k e m v,
       leftcontext RV RV C ->
@@ -229,7 +229,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       is_true v (typeof r1) ->
       typeof r2 = ty ->
       estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m)
-	 E0 (ExprState f (C (Eparen r2 ty)) k e m)
+         E0 (ExprState f (C (Eparen r2 ty)) k e m)
 
   | step_condition_false: forall f C r1 r2 r3 ty k e m v,
       leftcontext RV RV C ->
@@ -237,7 +237,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       is_false v (typeof r1) ->
       typeof r3 = ty ->
       estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m)
-	 E0 (ExprState f (C (Eparen r3 ty)) k e m)
+         E0 (ExprState f (C (Eparen r3 ty)) k e m)
 
   | step_assign: forall f C l r ty k e m b ofs v v' m',
       leftcontext RV RV C ->
@@ -247,7 +247,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       store_value_of_type (typeof l) m b ofs v' = Some m' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassign l r ty)) k e m)
-	 E0 (ExprState f (C (Eval v' ty)) k e m')
+         E0 (ExprState f (C (Eval v' ty)) k e m')
 
   | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 m',
       leftcontext RV RV C ->
@@ -259,7 +259,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       store_value_of_type (typeof l) m b ofs v4 = Some m' ->
       ty = typeof l ->
       estep (ExprState f (C (Eassignop op l r tyres ty)) k e m)
-	 E0 (ExprState f (C (Eval v4 ty)) k e m')
+         E0 (ExprState f (C (Eval v4 ty)) k e m')
 
   | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 m',
       leftcontext RV RV C ->
@@ -270,7 +270,7 @@ Inductive estep: state -> trace -> state -> Prop :=
       store_value_of_type ty m b ofs v3 = Some m' ->
       ty = typeof l ->
       estep (ExprState f (C (Epostincr id l ty)) k e m)
-	 E0 (ExprState f (C (Eval v1 ty)) k e m')
+         E0 (ExprState f (C (Eval v1 ty)) k e m')
 
   | step_comma: forall f C r1 r2 ty k e m v,
       leftcontext RV RV C ->