diff options
| author | Emilio Jesus Gallego Arias | 2019-05-23 06:43:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:54:18 +0200 |
| commit | fb92bcc7830a084a4a204c4f58c44e83c180a9c9 (patch) | |
| tree | a15f3c1de459d675c08ddf05d5c495d04c93fbd9 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 1496099e8cf7c27ed4e4db8270606eda06b9b156 (diff) | |
[proof] Remove redundant universe declaration information.
This was already in the base proof object however not forwarded by
`close_proof`. thus it had to be stored twice.
There are more cases like this, like `poly`, all are covered by
subsequent commits.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions