summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:07:05 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:07:05 -0400
commita735f6ea0ef8ec5895dfe7f895f89ee8c126de14 (patch)
tree702dbe43701e15a37f7811983aad78e069812704 /src/elab_env.sml
parent43cd4231dea11d2cbb0151f144e4a98c618df396 (diff)
Destructing local let, to the point where demo compiles
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml20
1 files changed, 10 insertions, 10 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 88b2554b..2296d819 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1454,9 +1454,18 @@ fun projectConstraints env {sgn, str} =
| SgnError => SOME []
| _ => NONE
+fun patBinds env (p, loc) =
+ case p of
+ PWild => env
+ | PVar (x, t) => pushERel env x t
+ | PPrim _ => env
+ | PCon (_, _, _, NONE) => env
+ | PCon (_, _, _, SOME p) => patBinds env p
+ | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
+
fun edeclBinds env (d, loc) =
case d of
- EDVal (x, t, _) => pushERel env x t
+ EDVal (p, _, _) => patBinds env p
| EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
fun declBinds env (d, loc) =
@@ -1565,13 +1574,4 @@ fun declBinds env (d, loc) =
pushENamedAs env x n t
end
-fun patBinds env (p, loc) =
- case p of
- PWild => env
- | PVar (x, t) => pushERel env x t
- | PPrim _ => env
- | PCon (_, _, _, NONE) => env
- | PCon (_, _, _, SOME p) => patBinds env p
- | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
-
end