-Require Export Recursion.Monad.
-Require Export Recursion.Termination.
+Require Export Computation.Monad.
+Require Export Computation.Termination.
(* evaluate up to [n] computation steps *)
Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
-Require Import Recursion.Monad.
+Require Import Computation.Monad.
(* decomposition lemma *)
Definition decomp (A:Set)(c:#A) : #A :=
-all: Recursion/Eval.vo Recursion/Tactics.vo Recursion/Termination.vo Recursion/Monad.vo
+all: Computation/Eval.vo Computation/Tactics.vo Computation/Termination.vo Computation/Monad.vo
clean:; rm */*.vo
-Recursion/Termination.vo: Recursion/Monad.vo
-Recursion/Tactics.vo: Recursion/Monad.vo
-Recursion/Eval.vo: Recursion/Termination.vo
+Computation/Termination.vo: Computation/Monad.vo
+Computation/Tactics.vo: Computation/Monad.vo
+Computation/Eval.vo: Computation/Termination.vo
%.vo: %.v
- coqc -R Recursion Recursion $<
\ No newline at end of file
+ coqc -R Computation Computation $<
\ No newline at end of file