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 /plugins/romega/const_omega.mli | |
| 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 'plugins/romega/const_omega.mli')
| -rw-r--r-- | plugins/romega/const_omega.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index b4599c831..ca23ed6c4 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -43,9 +43,8 @@ val coq_p_imp : Term.constr lazy_t val coq_p_prop : Term.constr lazy_t val coq_s_bad_constant : Term.constr lazy_t -val coq_s_div_approx : Term.constr lazy_t +val coq_s_divide : Term.constr lazy_t val coq_s_not_exact_divide : Term.constr lazy_t -val coq_s_exact_divide : Term.constr lazy_t val coq_s_sum : Term.constr lazy_t val coq_s_merge_eq : Term.constr lazy_t val coq_s_split_ineq : Term.constr lazy_t |