X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction.v;fp=src%2FExtraction.v;h=d1c84e450a7693b5859442dabbee3ecd2667bb21;hp=43d404fa98169f42ca0c61e7eb48f160d9a205f1;hb=539d675a181f178e24c15b2a6ad3c990492eed79;hpb=8f00501ac48984925832279f7d67302c09a570ec

diff --git a/src/Extraction.v b/src/Extraction.v
index 43d404f..d1c84e4 100644
--- 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.