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/Cshmgenproof2.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/Cshmgenproof2.v')
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 4 |
1 files changed, 2 insertions, 2 deletions
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, |