diff options
| author | Gaëtan Gilbert | 2020-04-02 12:13:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-02 12:13:57 +0200 |
| commit | f7a5f8a46bbb39f7694990603be875f2ca466e7d (patch) | |
| tree | 475f8c3bdc928ff0a6f44133616df04d7376d1ab /plugins/syntax/float_syntax.ml | |
| parent | d03529ab8fec0cad5705b5f775e43ef26c0dedcb (diff) | |
Cleanup tactic_option a bit
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions