The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

> By the way, it is possible that the following is a bad use of
> functor types :-(

 I forgot to add: yes, basically it is. I have not found yet any
 use for functor types. What you want to do is probably:

Module Type S1.
 Parameter t : Set.
 Parameter eq_dec : forall a b:t, {a=b}+{a<>b}.
End S1.
 
Module Type S2 (M:S1).
 Declare Module M: S1.
 Definition t := M.t.
 Definition eq_dec := M.eq_dec.
 Parameter eq_dec_prop : forall a b:t, a = b \/ a <> b.
End S2.

Module F1_2 (M:S1) : S2 with Module M := M.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------