X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;fp=src%2FHaskCoreToWeak.v;h=6e1b58fc1ece127b932cc87933b9e7c87b49f634;hp=36399a06135585fdc91a9daef0a886db701f230f;hb=f07414f45d72f4228c64fb62ef2268f88ed1830a;hpb=fdebbea0c0303b8bba05779f2635c9a0e5c459b7

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 36399a0..6e1b58f 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -4,8 +4,8 @@
 
 Generalizable All Variables.
 Require Import Preamble.
-Require Import General.
 Require Import Coq.Lists.List.
+Require Import General.
 Require Import HaskKinds.
 Require Import HaskLiteralsAndTyCons.
 Require Import HaskCoreVars.
@@ -229,9 +229,9 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                       | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
                         OK (((WeakDataAlt dc),
-                        (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
-                        (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
-                        (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
                         e')::rest')
                     end
             end) alts)