diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-07 09:25:53 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-07 09:25:53 +0200 |
commit | 584eac7027cd4d29c5ca8744453ffeea8f18b501 (patch) | |
tree | 374cd5c593eae420ff4e14e73de4c73709a6a87e /runtime/include/varargs.h | |
parent | 9f30d4984863ec655a03996646805202dc2a07c9 (diff) | |
download | compcert-584eac7027cd4d29c5ca8744453ffeea8f18b501.tar.gz compcert-584eac7027cd4d29c5ca8744453ffeea8f18b501.zip |
Represent external worlds by a coinductive type rather than an inductive type.
As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
Diffstat (limited to 'runtime/include/varargs.h')
0 files changed, 0 insertions, 0 deletions