diff options
author | 2012-05-09 08:53:10 -0400 | |
---|---|---|
committer | 2012-05-09 08:53:10 -0400 | |
commit | aeff2f17cdd47ac4f0b6dbdcbc50ad85bd7216a7 (patch) | |
tree | 8841a7082f34965432d019b8bcce28e5cc329a70 /src | |
parent | b24e172e9e6f8e3e60e4ff36d018f8611a55090a (diff) |
In incremental elaboration, handle invalidated FFI signatures
Diffstat (limited to 'src')
-rw-r--r-- | src/mod_db.sml | 3 |
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), |