From: Adam Megacz Date: Fri, 25 Mar 2011 18:12:22 +0000 (-0700) Subject: change import order in HaskWeakVars X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=af8dfc24d60a82c1229af9ffcddf704eec2d14ce change import order in HaskWeakVars --- diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 61eafca..5169046 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -4,9 +4,9 @@ Generalizable All Variables. Require Import Preamble. -Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. +Require Import General. Require Import HaskKinds. Require Import HaskLiteralsAndTyCons. Require Import HaskCoreVars. @@ -44,7 +44,7 @@ Definition haskLiteralToWeakType lit : WeakType := Variable coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". Variable getTyConTyVars_ : CoreTyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "getTyConTyVars". Definition tyConTyVars (tc:CoreTyCon) := - General.filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). + filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). Opaque tyConTyVars. Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).