diff options
| author | Pierre-Marie Pédrot | 2021-03-12 13:17:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-16 20:02:56 +0100 |
| commit | 22be1892ee1b6030cfe9406bf72bb320dbe68be7 (patch) | |
| tree | c0ff49ac14f24c338bf0953c53959d41b950fb0c /plugins/syntax/float_syntax.ml | |
| parent | 761d3ccaf6a593a73811da38fa731c2f601902f8 (diff) | |
Slightly richer API allowing to shift the inductive in a block.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions