The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 26 Mar 2007, 
roconnor AT theorem.ca
 wrote:

> So I suspect that I cannot have a type of uniformly continuous functions that 
> is automatically coerced into both a metric space and a Funclass. But maybe 
> someone knows a trick using identity coercions and or canonical structures 
> that can solve this problem.

Nevermind.  Everything actually works perfectly fine with all my 
coercions.  The problem was that I had defined another coercion elsewhere 
that was interfering with the existing coercions.  I've removed that other 
coecrion.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''