X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=Computation%2FTactics.v;fp=Recursion%2FTactics.v;h=c7108178300e1528c74510d17f73b8e4639e76e6;hp=bf441dfe190048f3de1e2ad5a6f1e4cd178e0fff;hb=ad8905d391e4e2015b6525a81a3b5e1ad607439e;hpb=7439e43c33a10817e19e7a5f26435d2097dc262d;ds=sidebyside

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 :=