diff options
| author | Emilio Jesus Gallego Arias | 2019-10-24 20:31:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-28 17:02:32 +0100 |
| commit | b27f54b04f50d3fad0eedd9c46366fd2bb612987 (patch) | |
| tree | 3e501d91de1ca811786e835a598b1d4220fb65e7 /dev/include_dune | |
| parent | 42eac2b1cee72acce4ebf0ce3e74dd60763b223b (diff) | |
[declare] Provide helper for private constant inlining.
We factor some duplicate code, this is a step towards making the
`proof_entry` type abstract.
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions