aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-07-19 18:55:05 +0200
committerEmilio Jesus Gallego Arias2019-07-23 14:31:10 +0200
commitd407d1f3f2f877fca8673eaf0470b3390e55dbaa (patch)
tree5493ae8ba45ef916d14c1e90d722da2aadf801c0 /dev/ci/ci-basic-overlay.sh
parentd68f695b5a953c50bcf5e80182ef317682de1a05 (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 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions