summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-11-24 09:56:50 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2013-11-24 09:56:50 -0500
commit26606137b3c996ce9d51adb12d95b75536d3ab8b (patch)
tree47f79f76bd134cb196c115fe742c4552cb5b27a0
parenta4d5ba7b1f751a615297a275819ee7058535196b (diff)
Sneaky still-in-today's-release update of 'table' signature item handling
-rw-r--r--src/elaborate.sml6
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