diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2013-11-24 09:56:50 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2013-11-24 09:56:50 -0500 |
| commit | 648f59ef006f7e0493f39f6936b14a66403ec1d4 (patch) | |
| tree | 47f79f76bd134cb196c115fe742c4552cb5b27a0 /src/elaborate.sml | |
| parent | 4bc1692a3dfe9f08dda07a192375f8e3ed3a0fe5 (diff) | |
Sneaky still-in-today's-release update of 'table' signature item handling
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 9906cf92..dfa8d0e2 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2629,7 +2629,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = checkCon env' ce' cet cst; ([(L'.SgiConAbs (x', hidden_n, cstK), loc), - (L'.SgiConstraint (visible, hidden), loc), + (L'.SgiConstraint ((L'.CConcat (pkey, visible), loc), hidden), loc), (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) end @@ -3631,7 +3631,7 @@ and wildifyStr env (str, sgn) = NONE => NONE | SOME c' => SOME (L.TRecord c', loc)) - | c => (Print.preface ("WTF?", p_con env (c, loc)); NONE) + | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) fun buildNeeded env sgis = #1 (foldl (fn ((sgi, loc), (nd, env')) => @@ -4860,6 +4860,8 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = ModDb.revert () else (); + + (*Print.preface("File", ElabPrint.p_file env file);*) (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds |