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

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.