summaryrefslogtreecommitdiff
path: root/driver/Complements.v
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Complements.v')
-rw-r--r--driver/Complements.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Complements.v b/driver/Complements.v
index 938c488..8ee70bd 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -51,7 +51,7 @@ Require Import Errors.
that this external call succeeds, has result [r], and changes
the world to [w]. *)
-Inductive world: Set :=
+Inductive world: Type :=
World: (ident -> list eventval -> option (eventval * world)) -> world.
Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :