comparison src/elaborate.sml @ 93:94afff1ff7f6

More fun with HTML
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 17:14:35 -0400
parents 1a4c51fa615c
children f0f59e918cac
comparison
equal deleted inserted replaced
92:1a4c51fa615c 93:94afff1ff7f6
1808 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) 1808 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
1809 end 1809 end
1810 1810
1811 | L.DStr (x, sgno, str) => 1811 | L.DStr (x, sgno, str) =>
1812 let 1812 let
1813 val () = if x = "Basis" then
1814 raise Fail "Not allowed to redefine structure 'Basis'"
1815 else
1816 ()
1817
1813 val formal = Option.map (elabSgn (env, denv)) sgno 1818 val formal = Option.map (elabSgn (env, denv)) sgno
1814 1819
1815 val (str', sgn', gs') = 1820 val (str', sgn', gs') =
1816 case formal of 1821 case formal of
1817 NONE => 1822 NONE =>