summaryrefslogtreecommitdiff
path: root/src/expl_env.sml
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2014-05-27 21:38:01 -0400
committerGravatar Ziv Scully <ziv@mit.edu>2014-05-27 21:38:01 -0400
commitdc336268adfbf2b05b34ab006de5990f8ce9086c (patch)
tree22fb72ef5ad32f47571fa250515108188d7e22f9 /src/expl_env.sml
parentd941d873c0203009ccf44aa4aed97671703ca375 (diff)
parent4cee29f03879d25963e3d8a8dda879e0a007033c (diff)
Merge.
Diffstat (limited to 'src/expl_env.sml')
-rw-r--r--src/expl_env.sml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/expl_env.sml b/src/expl_env.sml
index f5a5eb0a..5712a72d 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -346,6 +346,7 @@ fun declBinds env (d, loc) =
| DTask _ => env
| DPolicy _ => env
| DOnError _ => env
+ | DFfi (x, n, _, t) => pushENamed env x n t
fun sgiBinds env (sgi, loc) =
case sgi of