From 9ae1c2904195960575e414a3246b297237254f87 Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Mon, 23 Mar 2015 17:07:30 +0100
Subject: [PATCH] Update to the latest version of coq:io

---
 src/Main.v | 38 ++++++++++++++++++++------------------
 1 file changed, 20 insertions(+), 18 deletions(-)

diff --git a/src/Main.v b/src/Main.v
index 91cbb8d..dd61bb4 100644
--- a/src/Main.v
+++ b/src/Main.v
@@ -7,11 +7,11 @@ Import ListNotations.
 Import C.Notations.
 
 (** The classic Hello World program. *)
-Definition hello_world (argv : list LString.t) : C.t System.effects unit :=
+Definition hello_world (argv : list LString.t) : C.t System.effect unit :=
   System.log (LString.s "Hello world!").
 
 (** Ask for the user name and answer hello. *)
-Definition your_name (argv : list LString.t) : C.t System.effects unit :=
+Definition your_name (argv : list LString.t) : C.t System.effect unit :=
   do! System.log (LString.s "What is your name?") in
   let! name := System.read_line in
   match name with
@@ -21,7 +21,7 @@ Definition your_name (argv : list LString.t) : C.t System.effects unit :=
 
 (** A concurrent Hello World. May print "Hello World" or "World Hello". *)
 Definition concurrent_hello_world (argv : list LString.t)
-  : C.t System.effects unit :=
+  : C.t System.effect unit :=
   let! _ : unit * unit := join
     (System.log (LString.s "Hello"))
     (System.log (LString.s "World")) in
@@ -34,34 +34,36 @@ Extraction "extraction/main" main.
 
 (** Specifications. *)
 Module Run.
+  Import Io.Spec.
+
   (** The Hello World program only says hello. *)
   Definition hello_world_ok (argv : list LString.t)
-    : Run.t (hello_world argv) tt.
-    apply (Run.log_ok (LString.s "Hello world!")).
+    : Spec.t (hello_world argv) tt.
+    apply (Spec.log_ok (LString.s "Hello world!")).
   Defined.
 
   (** The Your Name program answers something when you give your name. *)
   Definition your_name_ok (argv : list LString.t) (name : LString.t)
-    : Run.t (your_name argv) tt.
-    apply (Run.Let (Run.log_ok _)).
-    apply (Run.Let (Run.read_line_ok name)).
-    apply (Run.log_ok _).
+    : Spec.t (your_name argv) tt.
+    apply (Let (Spec.log_ok _)).
+    apply (Let (Spec.read_line_ok name)).
+    apply (Spec.log_ok _).
   Defined.
 
   (** The Your Name program does nothing more in case of error on stdin. *)
   Definition your_name_error (argv : list LString.t)
-    : Run.t (your_name argv) tt.
-    apply (Run.Let (Run.log_ok _)).
-    apply (Run.Let Run.read_line_error).
-    apply Run.Ret.
+    : Spec.t (your_name argv) tt.
+    apply (Let (Spec.log_ok _)).
+    apply (Let Spec.read_line_error).
+    apply Ret.
   Defined.
 
   (** The concurrent Hello World program says both "Hello" and "World". *)
   Definition concurrent_hello_world_ok (argv : list LString.t)
-    : Run.t (concurrent_hello_world argv) tt.
-    apply (Run.Let (Run.Join
-      (Run.log_ok (LString.s "Hello"))
-      (Run.log_ok (LString.s "World")))).
-    apply Run.Ret.
+    : Spec.t (concurrent_hello_world argv) tt.
+    apply (Let (Join
+      (Spec.log_ok (LString.s "Hello"))
+      (Spec.log_ok (LString.s "World")))).
+    apply Ret.
   Defined.
 End Run.