diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-21 15:20:54 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-21 15:20:54 +0200 |
| commit | b686f8df572ea77c8832637bed4e4cd81f0931e2 (patch) | |
| tree | 49d7921708c2dbb874dd7b53d0d74d9416735cb2 /common | |
| parent | 2a26429f28bea6356521135c632ddb9a8b11c018 (diff) | |
| download | compcert-b686f8df572ea77c8832637bed4e4cd81f0931e2.tar.gz compcert-b686f8df572ea77c8832637bed4e4cd81f0931e2.zip | |
Ctyping: better typing of conditional expressions.
Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.
Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline. Then, retyping would
no longer be performed in C2C. We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.
Diffstat (limited to 'common')
0 files changed, 0 insertions, 0 deletions