projects
/
coq-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr
[coq-hetmet.git]
/
src
/
HaskCoreToWeak.v
diff --git
a/src/HaskCoreToWeak.v
b/src/HaskCoreToWeak.v
index
6fc5b43
..
a812483
100644
(file)
--- a/
src/HaskCoreToWeak.v
+++ b/
src/HaskCoreToWeak.v
@@
-200,7
+200,10
@@
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
>>= fun branches =>
coreExprToWeakExpr e >>= fun scrutinee =>
coreTypeToWeakType tbranches >>= fun tbranches' =>
>>= fun branches =>
coreExprToWeakExpr e >>= fun scrutinee =>
coreTypeToWeakType tbranches >>= fun tbranches' =>
- OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))
+ OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
end
end.
end
end.
+
+
+