The Coq mailing list

["Strub, Pierre-Yves" <pierre-yves AT strub.nu>]

Hi,

One way to work around this is to define your canonical structure on an 
alias of your type. See for example the left-module canonical structure 
for rings when these last are acting on themselves (Search for the 
notation "R ^o" in ssralg.v). You then have to give some type 
annotation, e.g.:

  Goal forall (R : ringType) (x y : {poly R}^o), x *: y = x * y.

choose the wanted lmodule structure for {poly R}. Note that R^o is 
convertible to R.

Best,
-- Pierre-Yves.

On 2014-06-18 00:56, Peng Wang wrote:
> Is there a way to remove or update a canonical structure registration?
>
> For example, SSReflect's matrix.v registers a canonical structure
> matrix_lmodType to declare that ring-element matrices form an L-module
> whose scalars are of the same type as the elements. But for
> algebra-element matrices, there is another way to form an L-module,
> where scalars are from the underlying ring of the algebra. I want to
> register this alternative L-module structure to be canonical (e.g. to
> talk about "a matrix of functions scaled by a constant"), but Coq's
> Canonical Structure command only respects the first registration and
> ignores later ones.