diff options
| author | Emilio Jesus Gallego Arias | 2019-07-19 18:55:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-23 14:31:10 +0200 |
| commit | d407d1f3f2f877fca8673eaf0470b3390e55dbaa (patch) | |
| tree | 5493ae8ba45ef916d14c1e90d722da2aadf801c0 /plugins/syntax/string_notation.ml | |
| parent | d68f695b5a953c50bcf5e80182ef317682de1a05 (diff) | |
[vernacexpr] Remove duplicate fixpoint record.
We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.
This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions