The Coq mailing list

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

  Bonjour,

> j'utilise actuellement la version V6.3.1 de coq
> lorsque j'importe Ensembles et Polylist, je cree une surcharge de 
> l'operateur "In" puisqu'il est defini dans ces deux fichiers/sections.
> comment Coq gere-t-il le conflit ?

  Celui charge en dernier rend l'autre inaccessible par l'utilisateur.

> puis-je l'obliger a utiliser l'un ou l'autre de
> ces 2 operateurs ou bien ces 2 theories presentent actuellement une certaine
> incompatibilite ??...

  Si c'est pour utiliser In dans une definition, il y a une solution
un peu tordue : il faut redefinir le premier des "In" charge sous un
autre nom avant de charger le 2eme module redefinissant In. Par
exemple :

Require Ensembles.
Syntactic Definition belongs := (In ?).
Require PolyList.

Le In de Ensembles s'affichera alors sous la forme d'un nom long illisible :

Coq < Print belongs.
 Syntax Macro belongs = (#GENTERM (CONST #Ensembles#In.cci) ?)

mais sera accessible en utilisant belongs.

Pour ameliorer l'affichage if faut lancer l'incantation suivante :

Syntax constr
  level 1:
  my_in [ (CONST #Ensembles#In.cci) ] -> [ "belongs" ].


Cependant, dans une preuve, le "Unfold belongs" ne sera pas reconnu.
Il faudra alors contourner le probleme et utiliser un "Red" ou un "Change".


Ceci dit, la constante "In" est assez formelle, (In P x) peut
supporter de s'ecrire (P x).

                                                  Hugo

"Demain", il y aura des modules dans Coq qui permettront des noms
qualifies.