require all branches of LetRec be at the same level in HaskProof

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

diff --git a/src/Extraction.v b/src/Extraction.v
index 43d404f..d1c84e4 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -230,7 +230,6 @@ Section core2proof.
 (*
     Definition TInt : HaskType nil ★.
       assert (tyConKind' intPrimTyCon = ★).
-        admit.
         rewrite <- H.
         unfold HaskType; intros.
         apply TCon.