diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-11 15:16:21 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-11 15:20:29 +0200 |
| commit | 06f3ce00971283d2718e272ec9f123430d75ffa6 (patch) | |
| tree | e25604900163c161ef28c1aaf08714aa957c4bf9 /CHANGES | |
| parent | 91d78c590b35c9edcf9f68c408ba82090f68e156 (diff) | |
Documenting Printing Compact Contexts + CHANGES
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -19,6 +19,12 @@ Tactics be fairly uncommon. - "auto with real" can now discharge comparisons of literals +Vernacular Commands + +- Goals context can be printed in a more compact way when "Set + Printing Compact Contexts" is activated. + + Standard Library - New file PropExtensionality.v to explicitly work in the axiomatic |