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/Cshmgenproof1.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'cfrontend/Cshmgenproof1.v')

diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 7ffd156..b86b09b 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -17,7 +17,7 @@ Require Import Cminor.
 Require Import Csharpminor.
 Require Import Cshmgen.
 
-(** Operations on types *)
+(** * Properties of operations over types *)
 
 Lemma transl_fundef_sig1:
   forall f tf args res,
@@ -65,7 +65,7 @@ Proof.
   simpl; intro EQ; inversion EQ; subst vk; auto.
 Qed.
 
-(** ** Some properties of the translation functions *)
+(** * Properties of the translation functions *)
 
 Lemma map_partial_names:
   forall (A B: Set) (f: A -> res B)
@@ -162,7 +162,7 @@ Proof.
   reflexivity.
 Qed.
 
-(** Transformation of expressions and statements *)
+(** Transformation of expressions and statements. *)
 
 Lemma is_variable_correct:
   forall a id,
@@ -209,7 +209,7 @@ Proof.
   rewrite EQ1; rewrite EQ0; rewrite EQ2; auto.
 Qed.
 
-(** Properties related to switch constructs *)
+(** Properties related to [switch] constructs. *)
 
 Fixpoint lblstmts_length (sl: labeled_statements) : nat :=
   match sl with
-- 
cgit v1.2.3