Mercurial > urweb
diff src/expl_env.sml @ 1278:cd8d2c73ccf4
Catch a missed ReduceLocal of field projection annotations
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 13 Jun 2010 14:13:06 -0400 |
parents | c316ca3c9ec6 |
children | b4480a56cab7 |
line wrap: on
line diff
--- a/src/expl_env.sml Sun Jun 13 10:55:20 2010 -0400 +++ b/src/expl_env.sml Sun Jun 13 14:13:06 2010 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -400,4 +400,13 @@ | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn | SgiStr (x, n, sgn) => pushStrNamed env x n sgn +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