Cshmgen: fixed the formatting of documentation comments

Author: xavierleroy

cfrontend/Cshmgen.v

@@ -615,11 +615,11 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: list type)
     returned by casting it to the return type of the function.
     For example, in the x86 ABI, a return value of type "char" is
     returned in register AL, leaving the top 24 bits of EAX
-    unspecified.  Hence, a cast to type "char" is needed to sign- or
+    unspecified.  Hence, a cast to type [char] is needed to sign- or
     zero-extend the returned integer before using it.
-    Function results of type "_Bool" are generally returned as
+    Function results of type [_Bool] are generally returned as
     one byte that is equal to 0 or to 1.  Hence, the appropriate normalization
-    is a cast to "unsigned char", not to "_Bool". *)
+    is a cast to [unsigned char], not to [_Bool]. *)
 
 Definition make_normalization (t: type) (a: expr) :=
   match t with
@@ -664,6 +664,7 @@ loop s1 s2          --->     block {
                                }
                              }
                              // break in s1 and s2 branches here
+>>
 *)
 
 Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)