rename Recursion

darcs-hash:20071002123310-5007d-2810fa6c7b014f9bebe5f7bb6730e5c7382fdff4.gz

diff --git a/Recursion/Eval.v b/Computation/Eval.v
similarity index 89%
rename from Recursion/Eval.v
rename to Computation/Eval.v
index 6c9b016..07d79e4 100644 (file)
--- a/Recursion/Eval.v
+++ b/Computation/Eval.v
@@ -1,5 +1,5 @@
-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 :=
 
 (* evaluate up to [n] computation steps *)
 Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=

diff --git a/Recursion/Monad.v b/Computation/Monad.v
similarity index 100%
rename from Recursion/Monad.v
rename to Computation/Monad.v

diff --git a/Recursion/Tactics.v b/Computation/Tactics.v
similarity index 96%
rename from Recursion/Tactics.v
rename to Computation/Tactics.v
index bf441df..c710817 100644 (file)
--- a/Recursion/Tactics.v
+++ b/Computation/Tactics.v
@@ -1,4 +1,4 @@
-Require Import Recursion.Monad.
+Require Import Computation.Monad.

 
 (* decomposition lemma *)
 Definition decomp (A:Set)(c:#A) : #A := 
 
 (* decomposition lemma *)
 Definition decomp (A:Set)(c:#A) : #A := 

diff --git a/Recursion/Termination.v b/Computation/Termination.v
similarity index 99%
rename from Recursion/Termination.v
rename to Computation/Termination.v
index 4d47a4a..d20d57a 100644 (file)
--- a/Recursion/Termination.v
+++ b/Computation/Termination.v
@@ -1,4 +1,4 @@
-Require Import Recursion.Monad.
+Require Import Computation.Monad.

 Require Import Coq.Logic.JMeq.
 
 Section Termination.
 Require Import Coq.Logic.JMeq.
 
 Section Termination.

diff --git a/Makefile b/Makefile
index 0bd72d5..bef71fe 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,10 @@
 
 

-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
 
 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
 
 %.vo: %.v

-       coqc -R Recursion Recursion $<
\ No newline at end of file
+       coqc -R Computation Computation $<
\ No newline at end of file