diff options
| author | Matthieu Sozeau | 2015-10-29 15:11:29 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-29 15:18:16 -0400 |
| commit | a3a17b514a2ffaba54cd182fdf27b7e84366ab44 (patch) | |
| tree | 8d48786996f4a8217404fbd43f3fdc72f922592f /kernel | |
| parent | 78edfe09f34db4a28fb41a1f6fd3bb4922d09ec8 (diff) | |
Handle side-effects of Vernacular commands inside proofs better, so that
universes are declared correctly in the enclosing proofs evar_map's.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions