[pretty-printing]: pretty-print in the theory environment of the targ…

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs

MIT License

306 stars 46 forks source link

[pretty-printing]: pretty-print in the theory environment of the targ… #560

Closed strub closed 2 months ago

strub commented 2 months ago

…et object

The theory environment is the environment obtained just before the theory is closed. This environment is now saved when a theory is closed (regardless of the theory being abstract or not).

This fixes two bugs:

hard failures when printing an abstract theory
long-object names

strub commented 2 months ago

See #51, #181

strub commented 2 months ago

The printing is done in the environment just before the theory is closed. So I would say that this is a feature (tm) :)