diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml index ea395a42ef1aa19c58aa4a70f9269ef7fcfc6024..304e4eabaad1e6fed91c230525546a341a383d3a 100644 --- a/src/plugins/qed/term.ml +++ b/src/plugins/qed/term.ml @@ -1327,7 +1327,7 @@ struct and i_affine_ratio_leq c xs ys = try match i_ratio xs , i_ratio ys with | POS(a,k) , NONE -> - (* c + a/k <= ys <==> a/k <= -c+ys *) + (* c + a/k <= ys <==> a/k <= -c+ys *) i_ratio_max a k (Z.neg c,ys) | NEG(a,k) , NONE -> (* c - a/k <= ys <==> c-ys <= a/k *)