The Coq mailing list

[Jasper Stein <jasper AT cs.ru.nl>]

Dear Coq-Club,

Since no one has answered my last week's question on why Raxioms.v defines 
the 
injection INR with a separate clause S O => 1, I have now turned to trying to 
compile a version without it. However, black magic and scrying ensue - and 
I'd be grateful if anyone could tell me how it's done (or answer my previous 
question - or, preferably, both).

Basically, my question is this: how does Coq know that when I type 0, I mean 
R0?

Consider the following transcript:
==========
jasper@Gainsay:~/coq-8.0pl3/theories/Reals$
 coqtop
Welcome to Coq 8.0pl3 (Jan 2006)

Coq < Check 0%R.
Toplevel input, characters 6-9
> Check 0%R.
>       ^^^
User error: Unknown scope delimiting key R

Coq < Require Export Rdefinitions.

Coq < Unset Printing Notations.

Coq < Set Printing Coercions.

Coq < Check 0%R.
R0
     : R
===========

Now one would think there's a Notation or Syntactic Definition command 
somewhere - but there isn't! And stranger still, if I make a copy of 
Rdefinitions (where R0 is defined), and only change R_scope into MyR_scope 
throughout, I can do this:

============
jasper@Gainsay:~/coq-8.0pl3/theories/Reals$
 coqtop
Welcome to Coq 8.0pl3 (Jan 2006)

Coq < Add LoadPath "/home/jasper/coq/MyReals".

Coq < Require Export MyRdefinitions.

Coq < Check 0%R.
0
     : nat
=============

So indeed the scope key R is defined, but it isn't bound to MyR_scope or to 
the type R.

Clarification, anyone? Or is this a bug?

Groeten,
-- 
Jasper Stein