From 9bf766d4f66727a638ed2662099d090b5a72200a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 23 May 2017 15:12:05 +0200 Subject: 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. --- plugins/romega/const_omega.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/romega/const_omega.mli') 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 -- cgit v1.2.3