X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=3dee0fecf5967ce4e9a600c0f91822a2ae7287d2;hp=f907514838bd9106a2e0af3b59ac8f4c8ea6ff4a;hb=97552c1a6dfb32098d4491951929ab1d4aca96a0;hpb=92e148ed7a7b0068cf2029537b019a88a7b07d43

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index f907514..3dee0fe 100644
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -507,13 +507,6 @@ Section HaskProofToStrong.
     admit.
     Defined.
 
-  Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
-    match t with
-      | T_Leaf None     => return []
-      | T_Leaf (Some x) => bind x' = x ; return [x']
-      | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
-    end.
-
   Definition gather_branch_variables
     Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
                 ProofCaseBranch tc Γ Δ lev tbranches avars sac})