diff options
| author | Pierre-Marie Pédrot | 2019-12-10 09:44:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-10 10:53:54 +0100 |
| commit | 5ccf803a86bc46d67038f4d33d26d5c9e899027f (patch) | |
| tree | 45fc5c34c1054ad7c5cf7989642911b784217223 /plugins/setoid_ring/plugin_base.dune | |
| parent | 50221b84f6af681f69e8f9847a851329a4662509 (diff) | |
Side-effect free wrapper around already declared schemes.
Some calls are actually guarded by a check that the scheme is already in
the cache. There is no reason to generate dummy side-effects in that case.
Diffstat (limited to 'plugins/setoid_ring/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions