X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=9d8dd4d970816458b0e4e6125c8d0cb9fc59f234;hp=6b6c7560ccfd0dfcc010bb3a61d0430beb9b6c29;hb=16fef762b0a81544a31b6392059d148431e984be;hpb=4c5c94487aa2bf5489371f112607f0a4c4f01a94;ds=sidebyside

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 6b6c756..9d8dd4d 100644
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -236,7 +236,6 @@ Section HaskSkolemizer.
       | 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 _
@@ -351,14 +350,6 @@ Section HaskSkolemizer.
         apply γ.
         apply (Prelude_error "found RCast at level >0").
 
-      destruct case_RJoin.
-        simpl.
-        destruct l.
-        apply nd_rule.
-        apply SFlat.
-        apply RJoin.
-        apply (Prelude_error "found RJoin at level >0").
-
       destruct case_RApp.
         simpl.
         destruct lev.