diff src/elab_env.sml @ 447:b77863cd0be2

Elaborating 'let'
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 11:17:29 -0400
parents cb5897276abf
children 85819353a84f
line wrap: on
line diff
--- a/src/elab_env.sml	Sat Nov 01 10:47:10 2008 -0400
+++ b/src/elab_env.sml	Sat Nov 01 11:17:29 2008 -0400
@@ -1075,6 +1075,11 @@
       | SgnError => SOME []
       | _ => NONE
 
+fun edeclBinds env (d, loc) =
+    case d of
+        EDVal (x, t, _) => pushERel env x t
+      | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
+
 fun declBinds env (d, loc) =
     case d of
         DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)