Hi,

Jacques Garrigue a écrit :
> 
> [ Disclaimer: you can safely skip this message if you are not
>   interested in labels. It is about modalities of use for people who
>   want them. ]
> 
> To summarize recent posts by various people, there are two approaches
> for a universal mode:
> 
> * Take the label mode as a basis, and split libraries where needed to
>   avoid troubling non-labellers.
>   Labels, when present, are no longer optional.
> 
I would vote for this one.


> * Extend classic mode with commutation, and keep labels in libraries.
>   Labels are kept optional.

The problem with this one is that if you choose to use labels, nothing
(at least for the moment) prevents you to write code in an inconsistent
style (putting labels at some places and forgetting them at some
others).

> 
> So, is there no way out?
> Not completely, if we accept to start from strict unification:
[...]

I can not really assess if this solution is good. However, it sounds to
me like a hack. I am rather suspicious of hack, be they clever as long
as they are not proven harmless (through a metatheoretical study). What
are the chances then that we experience bad behaviours of this hack
because of a lack of good theoretical properties?

Judicaël.
-- 
Judicael.Courant@lri.fr, http://www.lri.fr/~jcourant/
(+33) (0)1 69 15 64 85
"Montre moi des morceaux de ton monde, et je te montrerai le mien"
Tim, matricule #929, condamné à mort.
http://rozenn.picard.free.fr/tim.html
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr