diff options
| author | Maxime Dénès | 2019-04-05 10:22:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-05 10:22:25 +0200 |
| commit | 8750682e367d7e78634bf88e667e4c9e7c3613d3 (patch) | |
| tree | 5a62ebfa1b482c37727ccca2ab18e088fb282ade /vernac/comProgramFixpoint.ml | |
| parent | be6f3a6234ee809dd3c290621d80c3280a41355e (diff) | |
Remove cache in Heads
This cache makes the pretyper depend on components that should morally
be higher-level (Libobject and co), so I'd like to see how critical this
cache is before taking any action.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions