From c0bc146622528e3d52534909f5ae5cd2e375da8f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 5 Aug 2007 13:41:45 +0000
Subject: Documentation

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Cshmgenproof2.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'cfrontend/Cshmgenproof2.v')

diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 8e2ce303..a75621ca 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -22,7 +22,7 @@ Section CONSTRUCTORS.
 
 Variable tprog: Csharpminor.program.
 
-(** Properties of the translation of [switch] constructs. *)
+(** * Properties of the translation of [switch] constructs. *)
 
 Lemma transl_lblstmts_exit:
   forall e m1 t m2 sl body n tsl nbrk ncnt,
@@ -57,7 +57,7 @@ Proof.
 Qed.
 
 
-(** Correctness of Csharpminor construction functions *)
+(** * Correctness of Csharpminor construction functions *)
 
 Lemma make_intconst_correct:
   forall n le e m1,
-- 
cgit