diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-06-17 18:53:39 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-06-17 18:53:39 +0200 |
| commit | b51cc596555dae929e75e4a02520f01d6f53978d (patch) | |
| tree | 7a43ce306cb641b85dab43e88ed757edb873eed2 /common | |
| parent | e503983cdc99c6038ada0d0b94f32f02d13210c8 (diff) | |
| parent | 0e9ededa8c1d194453f5113bf57c93d0803f03b1 (diff) | |
| download | compcert-b51cc596555dae929e75e4a02520f01d6f53978d.tar.gz compcert-b51cc596555dae929e75e4a02520f01d6f53978d.zip | |
Merge branch 'master' into json_export
Diffstat (limited to 'common')
| -rw-r--r-- | common/Determinism.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Determinism.v b/common/Determinism.v index d0099ba9..7ea19663 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -36,7 +36,7 @@ Require Import Behaviors. that this external call succeeds, has result [r], and changes the world to [w]. *) -Inductive world: Type := +CoInductive world: Type := World (io: ident -> list eventval -> option (eventval * world)) (vload: memory_chunk -> ident -> int -> option (eventval * world)) (vstore: memory_chunk -> ident -> int -> eventval -> option world). |