The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

Hello,

Imagine one wanted to define a notation for application.

Notation "e1 @@ e2" := (e1 e2)  (at level 10).

This doesn't work as expected as it confuses the treatment of implicit 
arguments. More precisely, implicit arguments that are not declared to be 
maximally inserted don't seem to be considered.

Implicit Arguments Some [[A]].
Check (Some @@ 4).
        (* Some 4  : option nat *)
Implicit Arguments Some [A].
Check (Some @@ 4).

The term "4" has type "nat" while it is expected to have type "Type".

Does anyone see a way to work this around?

Many thanks in advance,
-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France