X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;fp=src%2FHaskFlattener.v;h=d805de4c7ab308c4c362225c75e0cd7d8536c885;hp=c5587c158a34a562ae9bfdc122d1b4a4143a7e63;hb=a663de9a349ffe83a6c4fc10f1259f2fa6a915ed;hpb=c90b598203ef23bf8d44d6b5b4a5a4b5901039cf

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index c5587c1..d805de4 100644
--- 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).
@@ -1315,6 +1315,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 +1331,7 @@ Section HaskFlattener.
     intros.
     rewrite mapOptionTree_compose.
     rewrite mapOptionTree_compose.
-    apply flatten_proof.
+    apply flatten_skolemized_proof.
     apply skolemize_proof.
     apply X.
     Defined.