X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FEval.v;fp=Computation%2FEval.v;h=76934831c00083c7f70343bc042ba1b01b0fc7ce;hp=28a00a03129f6c35e96ccac2541b8b184c90efb8;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d;ds=sidebyside

diff --git a/Computation/Eval.v b/src/Computation/Eval.v
similarity index 73%
rename from Computation/Eval.v
rename to src/Computation/Eval.v
index 28a00a0..7693483 100644
--- a/Computation/Eval.v
+++ b/src/Computation/Eval.v
@@ -1,7 +1,7 @@
 Require Export Computation.Monad.
 Require Export Computation.Termination.
 
-(* evaluate up to [n] computation steps *)
+(** evaluate up to [n] computation steps *)
 Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
   match n with
     | O      => None
@@ -16,17 +16,10 @@ Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
       end
   end.
 
-Inductive Unit : Set := unit : Unit.
-
-(*
- * In theory we'd like to be able to do this (below), but it violates
- * the Prop/Set separation:
- *
- * "Elimination of an inductive object of sort Prop is not allowed on a
- *  predicate in sort Set because proofs can be eliminated only to
- *  build proofs."
+(** In theory we'd like to be able to do this (below), but it violates the Prop/Set separation.
  *)
-(*
+(**
+<<
 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
   match t with
     | (Terminates_intro t') =>
@@ -34,8 +27,13 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
         | (ex_intro x y) => x
       end
   end.
-*)
+ 
+ "Elimination of an inductive object of sort Prop is not allowed on a
+  predicate in sort Set because proofs can be eliminated only to
+  build proofs."
+>>*)
 
+Inductive Unit : Set := unit : Unit.
 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
   match eval' c Unit (Return unit) (termination_is_safe A c t) with
     | exist x pf => x
@@ -43,3 +41,4 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
 
 Implicit Arguments eval [A].
 Implicit Arguments bounded_eval [A].
+