summaryrefslogtreecommitdiff
path: root/src/mod_db.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-05-09 08:53:10 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-05-09 08:53:10 -0400
commitaeff2f17cdd47ac4f0b6dbdcbc50ad85bd7216a7 (patch)
tree8841a7082f34965432d019b8bcce28e5cc329a70 /src/mod_db.sml
parentb24e172e9e6f8e3e60e4ff36d018f8611a55090a (diff)
In incremental elaboration, handle invalidated FFI signatures
Diffstat (limited to 'src/mod_db.sml')
-rw-r--r--src/mod_db.sml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/mod_db.sml b/src/mod_db.sml
index 5e9e3342..6c89c114 100644
--- a/src/mod_db.sml
+++ b/src/mod_db.sml
@@ -109,6 +109,9 @@ fun insert (d, tm) =
DStr (_, n', _, _) =>
(byId := #1 (IM.remove (!byId, n'));
false)
+ | DFfiStr (_, n', _) =>
+ (byId := #1 (IM.remove (!byId, n'));
+ false)
| _ => raise Fail "ModDb: Impossible decl"
else
true) (!byName),