X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=d822dd6700cb7f959aae9b25c047a4e81e71427e;hp=d805de4c7ab308c4c362225c75e0cd7d8536c885;hb=171beb27508a340b24ab14837e72451d0b500805;hpb=1a562d1799fa63f750837833093cb9d6296d9fc1

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index d805de4..d822dd6 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -835,7 +835,6 @@ Section HaskFlattener.
       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
-      | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
       | RVoid    _ _       l           => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
@@ -931,12 +930,6 @@ Section HaskFlattener.
       apply flatten_coercion; auto.
       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 
-    destruct case_RJoin.
-      simpl.
-      destruct l;
-        [ apply nd_rule; apply RJoin | idtac ];
-        apply (Prelude_error "RJoin at depth >0").
-
     destruct case_RApp.
       simpl.