The Coq mailing list

[Tim Reed <tim.reed AT gmail.com>]

Hi,

I have been reading the theory files to help me understand the
available theories for cyclic integers. Ideally, I would to find or make 
a library that extracts directly into Ocaml int's or int32/64's. 

Upon reading theories/Numbers/Cyclic/Int31/Int31.v, I came across
a command I have not seen and cannot find documentation for: 
Register. 

As an example, there first occurrence looks like this:
    
    Register digits as int31 bits in "coq_int31" by True.

I found a reference in the source code (tactics/extratactics.ml4) that 
seems to make clear that the parser should accept this command but
I'm unclear what the purpose of this and whether/how I can use it in
my code.

Can anyone shed some light on this? Should this be added to the 
reference manual?

Regards,
Tim Reed.