summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-12-05 14:34:44 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-12-05 14:34:44 -0500
commit7626d99de97a3132a934bf6021916405313dd51c (patch)
tree7152a432408de9ffafbc32510b0daf77ccadcca6
parent6b9b07746ffdd3e3cec6e81287f1334038a41092 (diff)
Recursive hnormSgn for projections of signatures from modules
-rw-r--r--src/elab_env.sml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 1bd4e059..4636fda8 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1088,7 +1088,7 @@ and hnormSgn env (all as (sgn, loc)) =
sgn = sgn,
field = x} of
NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
- | SOME sgn => sgn
+ | SOME sgn => hnormSgn env sgn
end
| SgnWhere (sgn, x, c) =>
case #1 (hnormSgn env sgn) of