diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-24 10:31:30 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-12 15:15:45 +0200 |
| commit | 1fe90249916bcce13aa39f36aa39f90b0f98bf50 (patch) | |
| tree | 9d50aef1fe3fd4d8a60d085c7770416a7f3ce143 /ide/minilib.mli | |
| parent | 83a3abfa7de680f1a3279710e8f84721c32b7668 (diff) | |
zify: force reduction of (Z.max 0 0) and similar (fix #5439)
Turn some "simpl" into "compute". Also do the same for the few
"simpl (Z.of_nat ...)". This way, definition like Z.max are properly
reduced, and moreover zify isn't sensible anymore to the
"Arguments Z.of_nat : simpl never" that some user want (see also #5039).
Unfortunately, the compute we're using now still honor the "Opaque"
declarations, so a "Opaque Z.max" will block things again (see also #5374).
Diffstat (limited to 'ide/minilib.mli')
0 files changed, 0 insertions, 0 deletions