The Coq mailing list

[anoun AT labri.fr]

Hi everybody,
Let's define a simpl module type to describe finite multisets:
 Module Type MSet.
Parameter A:Set.  (* types  of elements *)
Paramater X:Set.
....
Parameter empty:X.
Parameter union :X->X->X.

....
(* here we define some notations *)
Notation "m1 'U' m2":=(union m1 m2) (at level 10):set_scope.
End MSet.

Suppose that we need to define a functor that takes two multisets as 
parameters
Module mset_funct (M1 M2:MSet).


....
End mset_funct.

Inside mset_funct, we are unable to use the notation defined within MSet at
least for both m1 and m2.
We can use partially the notation for m1 if we export this module
Export m1.
but the problem remains for m2.

Is there a way to solve that problem?

Particularly with PCoq, can we define a new rule for pretty printer that
replaces 'X.union *x1 *x2' by *x1 U *x2 and so for all modules X?

Thanks a lot in advance
Houda



----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.