diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-14 15:24:59 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-14 15:24:59 -0400 |
| commit | 9a65eddb59384f5784ed3ef0a641ca65b52645ce (patch) | |
| tree | 6c2cbea03ee39858bde49e54932e19e744ba84c6 /src/elab_env.sml | |
| parent | 14fbe79a3735e547f03cd8e95ca925fbdbb1841a (diff) | |
Elaborating 'SELECT *' queries
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 30 |
1 files changed, 12 insertions, 18 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 2d6afa4a..acd918ec 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -404,15 +404,12 @@ fun sgiBinds env (sgi, loc) = | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env - | SgiTable (x, n, c) => - (case lookupStr env "Basis" of - NONE => raise Fail "ElabEnv.sgiBinds: Can't find Basis" - | SOME (n, _) => - let - val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) - in - pushENamedAs env x n t - end) + | SgiTable (tn, x, n, c) => + let + val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end fun sgnSeek f sgis = let @@ -737,14 +734,11 @@ fun declBinds env (d, loc) = | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn | DConstraint _ => env | DExport _ => env - | DTable (x, n, c) => - (case lookupStr env "Basis" of - NONE => raise Fail "ElabEnv.declBinds: Can't find Basis" - | SOME (n, _) => - let - val t = (CApp ((CModProj (n, [], "table"), loc), c), loc) - in - pushENamedAs env x n t - end) + | DTable (tn, x, n, c) => + let + val t = (CApp ((CModProj (tn, [], "table"), loc), c), loc) + in + pushENamedAs env x n t + end end |