Last updates for release 1.5.v1.5

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

1 files changed, 9 insertions, 9 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index e0d05f21..ee134875 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -628,20 +628,20 @@ End EXPR.
 Inductive cont: Type :=
   | Kstop: cont
   | Kseq: statement -> cont -> cont
-       (* [Kseq s2 k] = after [s1] in [s1;s2] *)
+       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
   | Kwhile: expr -> statement -> cont -> cont
-       (* [Kwhile e s k] = after [s] in [while (e) s] *)
+       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
   | Kdowhile: expr -> statement -> cont -> cont
-       (* [Kdowhile e s k] = after [s] in [do s while (e)] *)
+       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
   | Kfor2: expr -> statement -> statement -> cont -> cont
-       (* [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
+       (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
   | Kfor3: expr -> statement -> statement -> cont -> cont
-       (* [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
+       (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
   | Kswitch: cont -> cont
-       (* catches [break] statements arising out of [switch] *)
-  | Kcall: option (block * int * type) ->   (* where to store result *)
-           function ->                      (* calling function *)
-           env ->                           (* local env of calling function *)
+       (**r catches [break] statements arising out of [switch] *)
+  | Kcall: option (block * int * type) ->   (**r where to store result *)
+           function ->                      (**r calling function *)
+           env ->                           (**r local env of calling function *)
            cont -> cont.
 
 (** Pop continuation until a call or stop *)