romega: avoid potential slowdown when changing concl by reified version

 On some benchmarks provided by Chantal Keller a long time ago,
 romega was abnormally slow compared to omega (or lia).
 It turned out that the change of concl by reified version was
 triggering unnecessary unfolds of Z.add, instead of unfolding
 ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by
 the various Parameter Inline : no more indirections, Z_as_Int.plus
 is directly Z.add.

 Also use Tactics.convert_concl_no_check for this "change", as
 recommended by PMP.

0 files changed, 0 insertions, 0 deletions