summaryrefslogtreecommitdiff
path: root/cfrontend/Cshmgenproof2.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/Cshmgenproof2.v')
-rw-r--r--cfrontend/Cshmgenproof2.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 8e2ce30..a75621c 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,