diff options
| author | Gaëtan Gilbert | 2018-03-02 15:10:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-03-06 13:42:31 +0100 |
| commit | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (patch) | |
| tree | e8c0b4a760bd008afde92ea1902a6e2c2ba3946b /dev/tools/pre-commit | |
| parent | 5d926b0279f70250db1ee54edcdb4e855ac96f0f (diff) | |
Rename some universe minimizing "normalize" functions to "minimize"
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions