diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 19:08:22 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 20:36:36 -0400 |
| commit | c9f7a31ef67ce638ec591f9e5760941706bc12bc (patch) | |
| tree | 21963d1559d6dca5d173f270e4a6b22d76369be4 /plugins/syntax/plugin_base.dune | |
| parent | d050094c578bdf5fc0611b808949fee28ae2a641 (diff) | |
[save proof] Declare universe_binders unconditionally for mutual assumptions.
As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions