diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-05 13:41:45 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-05 13:41:45 +0000 |
| commit | c0bc146622528e3d52534909f5ae5cd2e375da8f (patch) | |
| tree | 52c5f163a82b04d7ad56055b4bd5e852be168ae4 /cfrontend/Cshmgenproof1.v | |
| parent | adc9e990a0c338cef57ff1bd9717adcc781f283c (diff) | |
| download | compcert-c0bc146622528e3d52534909f5ae5cd2e375da8f.tar.gz compcert-c0bc146622528e3d52534909f5ae5cd2e375da8f.zip | |
Documentation
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof1.v')
| -rw-r--r-- | cfrontend/Cshmgenproof1.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index 7ffd156c..b86b09bf 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 |