Documentation

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 9 insertions, 3 deletions

diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 0795e1b2..cb572c09 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -1,4 +1,4 @@
-(** * Type well-formedness of C programs *)
+(** * Typing constraints on C programs *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -7,11 +7,14 @@ Require Import Csyntax.
 
 (** ** Typing rules *)
 
-(** This ``type system'' is very coarse: we check only the typing properties
+(** We now define a simple, incomplete type system for the Clight language.
+  This ``type system'' is very coarse: we check only the typing properties
   that matter for the translation to be correct.  Essentially,
   we need to check that the types attached to variable references
   match the declaration types for those variables. *)
 
+(** A typing environment maps variable names to their types. *)
+
 Definition typenv := PTree.t type.
 
 Section TYPING.
@@ -165,7 +168,10 @@ Record wt_program (p: program) : Prop :=  mk_wt_program {
     exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed)
 }.
 
-(** ** Type-checking algorithm *)
+(* ** Type-checking algorithm *)
+
+(** We now define and prove correct a type-checking algorithm
+  for the type system defined above. *)
 
 Lemma eq_signedness: forall (s1 s2: signedness), {s1=s2} + {s1<>s2}.
 Proof. decide equality. Qed.