The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

Actually, the problem observed is the result of a missing case in the
notation printing mechanism that is now fixed in 8.3 branch and trunk.

Hugo

On Wed, Jun 08, 2011 at 06:49:13PM +0200, Guillaume Brunerie wrote:
> 2011/6/8 Mehdi Dogguy 
>Â <mehdi AT dogguy.org>
> 
>     On 08/06/2011 17:03, Guillaume Brunerie wrote:
>     > The following does not work as expected:
>     >
>     > Parameter f : Type -> Type.
>     >> Notation s := (f Type).
>     >> Check s.
>     >>
>     >
> 
>     I could be wrong but isn't "Definition s := f Type" enough for your 
> needs?
>     (why do you need Notation?)
> 
> 
> Indeed, but in my case what I actually want is "Notation "#s" := (f Type)",
> because this term has a special meaning and I want to distinguish it from 
> the
> other identifiers in the script.
> I could have written "Definition  __s := (f Type)", or something like that, 
> but
> I find "#s" prettier than "__s" (and I need "Notation" for that).
> 
> 
> Guillaume