s/Eval/Evaluate/

coq-io · May 10, 2015 · 1e39ddf · 1e39ddf
1 parent 41af29c
commit 1e39ddf
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/Make b/Make
@@ -1,3 +1,3 @@
 -R src Io
 
-src/Eval.v
+src/Evaluate.v
diff --git a/src/Eval.v → src/Evaluate.v b/src/Eval.v → src/Evaluate.v
@@ -4,15 +4,15 @@ Require Import Io.All.
 Import C.Notations.
 
 (** Evaluate the commands of a computation. *)
-Fixpoint eval {E1 E2 : Effect.t} {A : Type}
+Fixpoint command {E1 E2 : Effect.t} {A : Type}
   (run : forall (c : Effect.command E1), C.t E2 (Effect.answer E1 c))
   (x : C.t E1 A) : C.t E2 A :=
   match x with
   | C.Ret _ x => C.Ret _ x
   | C.Call c => run c
-  | C.Let _ _ x f => C.Let _ _ (eval run x) (fun x => eval run (f x))
-  | C.Join _ _ x y => C.Join _ _ (eval run x) (eval run y)
-  | C.Choose _ x y => C.Choose _ (eval run x) (eval run y)
+  | C.Let _ _ x f => C.Let _ _ (command run x) (fun x => command run (f x))
+  | C.Join _ _ x y => C.Join _ _ (command run x) (command run y)
+  | C.Choose _ x y => C.Choose _ (command run x) (command run y)
   end.
 
 Fixpoint exception {E1 E2 : Effect.t} {Exc A : Type}