The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

In his message from Tuesday 4 May, 1999, Randy Pollack wrote: 
> What have I done wrong to see this this:
> 
>   Coq < Print eqs.
>   eqs = 
>   [T:CSetoid; n:nat; l,k:(listn (T) n)]
>    (i:(fin n))
>     (#GENTERM (CONST #listn#nth.cci) i l)
>        [=] (#GENTERM (CONST #listn#nth.cci) i k)
>        : (T:CSetoid; n:nat)(listn (T) n)->(listn (T) n)->Prop
> 
> Is it about Transparent/Opaque?
> 
> Randy

Dear Randy,

Not at all ! It is only about printing. There are 2 possibilities :

1) There is another constant called "nth" that hides the one from
module listn because it is more recent
2) The module listn is loaded but not visible (because you did
"Require A" with A containing "Require listn" and not "Require Export
listn"). Try the command "Require listn".

Patrick

-- 
Patrick.Loiseleur AT lri.fr