summaryrefslogtreecommitdiff
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
commit27d4abc1c11127eeae42c548dc142e1ffcd35dc0 (patch)
tree8841a7082f34965432d019b8bcce28e5cc329a70
parent53159b76f6717fab5165fd859f6caa8066951262 (diff)
In incremental elaboration, handle invalidated FFI signatures
-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),