X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=22f0e6042b254d84e56f688c2423ecd9a1ac67eb;hp=d5d66c0b7460b052e1fa28c9c52893aea810589e;hb=68f41d71d573b422b04ed3f4a3eb3ab41de09a79;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index d5d66c0..22f0e60 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -7,7 +7,8 @@ Require Import Preamble.
 Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 
@@ -19,6 +20,8 @@ Inductive WeakAltCon :=
 Inductive WeakExpr :=
 | WEVar       : WeakExprVar                                                  -> WeakExpr
 | WELit       : HaskLiteral                                                  -> WeakExpr
+
+(* TO DO: add a WEWhere and use the source location to detect which one the user used *)
 | WELet       : WeakExprVar -> WeakExpr         -> WeakExpr                  -> WeakExpr
 | WELetRec    : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr                  -> WeakExpr
 | WECast      : WeakExpr                        -> WeakCoercion              -> WeakExpr