diff options
author | Carst Tankink <carst.tankink@inria.fr> | 2014-10-09 15:39:08 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-13 18:13:21 +0200 |
commit | 0253fc47be156d0d87cccda32c5bb90bc37960da (patch) | |
tree | f5eac948b0a6eddceef5403185e5fb9760b8e628 /theories/Reals/R_Ifp.v | |
parent | e1ea8a70094dfed28223d02dfca5d768737d4421 (diff) |
When loading libraries, feed back dependencies.
These dependencies between files can be used by UIs to guide compilation
and reloading of files.
FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
Diffstat (limited to 'theories/Reals/R_Ifp.v')
0 files changed, 0 insertions, 0 deletions