From ad8905d391e4e2015b6525a81a3b5e1ad607439e Mon Sep 17 00:00:00 2001 From: adam Date: Tue, 2 Oct 2007 12:33:10 +0000 Subject: [PATCH] rename Recursion darcs-hash:20071002123310-5007d-2810fa6c7b014f9bebe5f7bb6730e5c7382fdff4.gz --- {Recursion => Computation}/Eval.v | 4 ++-- {Recursion => Computation}/Monad.v | 0 {Recursion => Computation}/Tactics.v | 2 +- {Recursion => Computation}/Termination.v | 2 +- Makefile | 10 +++++----- 5 files changed, 9 insertions(+), 9 deletions(-) rename {Recursion => Computation}/Eval.v (89%) rename {Recursion => Computation}/Monad.v (100%) rename {Recursion => Computation}/Tactics.v (96%) rename {Recursion => Computation}/Termination.v (99%) 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 --- 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 := 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 --- 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 := 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 --- 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. diff --git a/Makefile b/Makefile index 0bd72d5..bef71fe 100644 --- 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 -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 -- 1.7.10.4