remove RJoin rule

[coq-hetmet.git] / src / HaskFlattener.v

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index c5587c1..d822dd6 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -799,7 +799,7 @@ Section HaskFlattener.
     reflexivity.
     Qed.
 
-  Definition flatten_proof :
+  Definition flatten_skolemized_proof :
     forall  {h}{c},
       ND SRule h c ->
       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
@@ -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.
 
@@ -1315,6 +1308,13 @@ Section HaskFlattener.
       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
       Defined.
 
+  Definition flatten_proof :
+    forall  {h}{c},
+      ND  Rule h c ->
+      ND  Rule h c.
+    apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
+    Defined.
+
   Definition skolemize_and_flatten_proof :
     forall  {h}{c},
       ND  Rule h c ->
@@ -1324,7 +1324,7 @@ Section HaskFlattener.
     intros.
     rewrite mapOptionTree_compose.
     rewrite mapOptionTree_compose.
-    apply flatten_proof.
+    apply flatten_skolemized_proof.
     apply skolemize_proof.
     apply X.
     Defined.