The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

SAIBI Amokrane wrote:
> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


That works!

Thanks to you and Conor for helping me.

Cheers,
Pierre


--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran