Only backwards-compatible additions, so I could also have just pushed this, but I made a PR because I'm adding Require Import Coq.micromega.Lia. -- is that fine?
It adds hints about rational numbers, but nothing about real numbers, so auto with * might become a bit slower, and I'm not doing anything about that. Does anyone have experience with Set Loose Hint Behavior "Strict"., which might help here, but I didn't get to work as explained in https://github.com/mit-plv/bbv/pull/6?
Only backwards-compatible additions, so I could also have just pushed this, but I made a PR because I'm adding
Require Import Coq.micromega.Lia.-- is that fine?It adds hints about rational numbers, but nothing about real numbers, so
auto with *might become a bit slower, and I'm not doing anything about that. Does anyone have experience withSet Loose Hint Behavior "Strict"., which might help here, but I didn't get to work as explained in https://github.com/mit-plv/bbv/pull/6?