better comments/documentation

[coinductive-monad.git] / src / Computation / Tactics.v

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 (file)
--- a/Computation/Tactics.v
+++ b/src/Computation/Tactics.v
@@ -1,6 +1,6 @@
 Require Import Computation.Monad.
 
 Require Import Computation.Monad.
 

-(* decomposition lemma *)
+(** A decomposition lemma *)

 Definition decomp (A:Set)(c:#A) : #A := 
   match c with
     | Return x => Return x
 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.
 
   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. 
 
 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)] ] =>
 Ltac uncomp comp :=
   match goal with
     | [ |- context[(comp ?X)] ] =>