diff options
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 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 |