metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

Allow_growth -> may_grow #135

Closed GinoGiotto closed 1 year ago

GinoGiotto commented 1 year ago

The minimize command used to have an option called ALLOW_GROWTH which was replaced in 2019 with MAY_GROW, you can find evidence of this change in the metamath.c file:

4-Aug-2019 nm mmhlpb.c, mmcmdl.c, metamath.c - Add /ALLOW_NEW_AXIOMS,
renamed /ALLOW_GROWTH to /MAY_GROW

There is also a comment made by Norman Megill here where he said:

The qualifier "/allow_growth" will be changed to "/may_grow" (just a name change to reduce the number of characters you need to type to avoid ambiguity with "/allow_new_axioms").

There are a few lines in mmpfas.c that were left behind from this name change, so I updated them.