projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
fdebbea
)
change import order in HaskCoreToWeak
author
Adam Megacz
<megacz@cs.berkeley.edu>
Fri, 25 Mar 2011 18:12:03 +0000
(11:12 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Fri, 25 Mar 2011 18:12:03 +0000
(11:12 -0700)
src/HaskCoreToWeak.v
patch
|
blob
|
history
diff --git
a/src/HaskCoreToWeak.v
b/src/HaskCoreToWeak.v
index
36399a0
..
6e1b58f
100644
(file)
--- a/
src/HaskCoreToWeak.v
+++ b/
src/HaskCoreToWeak.v
@@
-4,8
+4,8
@@
Generalizable All Variables.
Require Import Preamble.
Generalizable All Variables.
Require Import Preamble.
-Require Import General.
Require Import Coq.Lists.List.
Require Import Coq.Lists.List.
+Require Import General.
Require Import HaskKinds.
Require Import HaskLiteralsAndTyCons.
Require Import HaskCoreVars.
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),
| 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)
e')::rest')
end
end) alts)