make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

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

diff --git a/src/Extraction.v b/src/Extraction.v
index 43d404f..c23d1c5 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -25,10 +25,10 @@ Require Import HaskProof.
 Require Import HaskCoreToWeak.
 Require Import HaskWeakToStrong.
 Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
 Require Import HaskProofToLatex.
 Require Import HaskStrongToWeak.
 Require Import HaskWeakToCore.
+Require Import HaskProofToStrong.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -230,7 +230,6 @@ Section core2proof.
 (*
     Definition TInt : HaskType nil ★.
       assert (tyConKind' intPrimTyCon = ★).
-        admit.
         rewrite <- H.
         unfold HaskType; intros.
         apply TCon.