Hi Sylvain, On Wed, Aug 04, 2010 at 08:15:15AM +0000, Sylvain Le Gall wrote: > I split the document already. > > Should I create a branch for that, or could it live in master? maybe the best would be to create a new branch for that. Thanks for your previous work on the policy! Amicalement -Ralf -- Ralf Treinen Laboratoire Preuves, Programmes et Systèmes Université Paris Diderot, Paris, France. http://www.pps.jussieu.fr/~treinen/