diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-23 15:12:05 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-24 15:20:42 +0200 |
| commit | 9bf766d4f66727a638ed2662099d090b5a72200a (patch) | |
| tree | fcd67b38cf8e367e5067c2fbe98f5cbc9b9d5ecc /test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | |
| parent | 60ca3fb1f2724f9a6d1b2e808a94a394711b7258 (diff) | |
ROmega: division-aware ReflOmegaCore, allowing trace without terms
The trace only mentions the constant k by which we want to divide
the equation, not anymore the equation we obtain after the division.
Shorter trace, and it won't take much more time to perform the few
Z.div than checking as currently the equality of the initial equation
and the final equation multiplied by k.
Diffstat (limited to 'test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v')
0 files changed, 0 insertions, 0 deletions