aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/plugin_base.dune
diff options
context:
space:
mode:
authorThéo Zimmermann2020-02-06 13:29:35 +0100
committerThéo Zimmermann2020-04-07 17:37:03 +0200
commit2e8e25217abe62ebf0ed17c3ef6c48f595699433 (patch)
tree60165c4e23af88352ab117f236d4d11b75383bac /plugins/funind/plugin_base.dune
parent2089207415565e8a28816f53b61d9292d04f4c59 (diff)
Support universe bindings and universe constraints in Let definitions.
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
Diffstat (limited to 'plugins/funind/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions