diff options
| author | Matej Kosik | 2015-10-29 10:41:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:09 +0100 |
| commit | 47c235b94e8870043deb04b65aad08eac8f7ae3e (patch) | |
| tree | 7e6413d994001f43c252164c6088b31e6a910dcf /dev/vm_printers.ml | |
| parent | cf7fb536777674b093ee1c5ac33126f75a55e12b (diff) | |
CLEANUP PROPOSITION: The 'pCIC' keyword from the 'Global Index' was removed.
We do not actually define the 'pCIC' concept in Chapter 4
so it does not make sense to keep an entry in the 'Global Index' for it.
Diffstat (limited to 'dev/vm_printers.ml')
0 files changed, 0 insertions, 0 deletions