The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi,

You have two options AFAIK: ask Ssreflect's devs to put the Canonical Instances in a module to import optionally, or to try some trick similar to the one we did in

http://www.mpi-sws.org/~beta/lessadhoc/

to deal with overlapping instances.

Right now I don't have the time to really look into your specific problem to help you out in a more direct way, but feel free to ask if you have any questions.

Best,

Beta

On Wed, Jun 18, 2014 at 12:56 AM, Peng Wang <wangp.thu AT gmail.com> 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.

Peng (Perry) Wang

--
Peng Wang (王鹏)

CSAIL, The Stata Center, MIT

77 Massachusetts Ave, 32-G822

Cambridge, MA 02139

Phone: (617)803-2025

Email: wangpeng AT csail.mit.edu