The Coq mailing list

["SAIBI Amokrane" <A.SAIBI AT oberthurcs.com>]

Hello,
You can try to use "Canonical structures" mechanism (reference manual 2.6.10) 
that can "maybe" solve the problem.
You must declare sigma as a "Canonical structure"
        Canonical Structure sigma.
Its effect is to add Hints to the "implicits" resolution algorithm: 
        (V ?) = vars => ? = sigma
        (C ?) = consts => ? = sigma
It is heavily used in the Category Therory formalisation and it is described 
in my thesis for this purpose and also
to simulate "lexical overloading".
best regards,
---
Amokrane SAÏBI