X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FTactics.v;fp=Computation%2FTactics.v;h=67ed175a2318b6d581450273b556f1e6e6b35cbe;hp=c7108178300e1528c74510d17f73b8e4639e76e6;hb=HEAD;hpb=bb471fbb694313a6aa61816752bd179b3af6711d

diff --git a/Computation/Tactics.v b/src/Computation/Tactics.v
similarity index 85%
rename from Computation/Tactics.v
rename to src/Computation/Tactics.v
index c710817..67ed175 100644
--- a/Computation/Tactics.v
+++ b/src/Computation/Tactics.v
@@ -1,6 +1,6 @@
 Require Import Computation.Monad.
 
-(* decomposition lemma *)
+(** A decomposition lemma *)
 Definition decomp (A:Set)(c:#A) : #A := 
   match c with
     | Return x => Return x
@@ -8,12 +8,12 @@ Definition decomp (A:Set)(c:#A) : #A :=
   end.
 Implicit Arguments decomp.
 
-(* decomposition theorem: we can always decompose *)
+(** A decomposition theorem: we can always decompose *)
 Theorem decomp_thm : forall (A:Set)(c:#A), c = decomp c.
   intros A l; case l; simpl; trivial. 
 Qed. 
 
-(* 1-, 2-, 3-, 4-, and 5-ary decompositions *)
+(** 1-, 2-, 3-, 4-, and 5-ary decompositions; you should use this *)
 Ltac uncomp comp :=
   match goal with
     | [ |- context[(comp ?X)] ] =>