summaryrefslogtreecommitdiff
path: root/coq
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-04 15:08:29 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-04 15:08:29 +0000
commit73729d23ac13275c0d28d23bc1b1f6056104e5d9 (patch)
treee3044ce75edb30377bd8c87356b7617eba5ed223 /coq
parentc79434827bf2bd71f857f4471f7bbf381fddd189 (diff)
Fusion de la branche "traces":
- Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'coq')
0 files changed, 0 insertions, 0 deletions