Polynomial coefficients with *: don't get recognized automatically -- one has to call -!mul_polyC by hand

[SnarkBoojum]

Here is a trivial example:

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.real_closed Require Import realalg.
From mathcomp.algebra_tactics Require Import ring.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory GRing.

Local Open Scope ring_scope.

Section Example.

Definition R := { realclosure rat }.
Definition RX := { poly R }.

Definition Psum := (4%:R *: 'X^3 - 3%:R *: 'X + 1%:P) : RX.
Definition Pprod := ('X + 1%:P) * (2%:R *: 'X - 1%:P) ^+ 2 : RX.

Lemma single_P: Psum = Pprod.
Proof.
  unfold Pprod.
  unfold Psum.
  rewrite -!mul_polyC. (* should be done by ring? *)
  by ring.
Qed.

End Example.

[pi8027]

Thanks. I will take a look.

[pi8027]

@SnarkBoojum FYI, I documented the tactics provided by this package in README. This documentation includes the lists of operators supported by the preprocessors. I hope it clarifies the fact that the preprocessor of the ring tactic does not support GRing.scale.

I know that it is technically possible to add support for GRing.scale. However, we also face a maintainability issue as the preprocessor becomes bigger (see common.v and common.elpi). So, I don't extend the preprocessors further until we find a fundamental solution to this maintainability issue.

[pi8027]

Since #79 subsumes this issue, I will close this issue unless there is opposition.

[SnarkBoojum]

That's fine with me - thanks