X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofFlattener.v;h=fcc2a37a78d865fe4500131e4df63eb888fc72bc;hp=82bc678dae88477b25efe0ce616db5741df9fb0f;hb=77e8c70f4fd7a32db036fee5884a98208d450de2;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v
index 82bc678..fcc2a37 100644
--- a/src/HaskProofFlattener.v
+++ b/src/HaskProofFlattener.v
@@ -133,6 +133,7 @@ Section HaskProofFlattener.
    * it might help to have the definition for "Inductive ND" (see
    * NaturalDeduction.v) handy as a cross-reference.
    *)
+(*
   Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
     : forall h c,
       (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) ->
@@ -392,6 +393,6 @@ Section HaskProofFlattener.
       *)
 
   (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
-
+*)
 End HaskProofFlattener.