Hi,

Thanks for your answers. Thanks to Damien for the handy
workarounds and to Boris for the sevral insightful comments.

I'll probably switch to the svn version, waiting for 3.12...

I think 3.13 was a typo, see:
  http://caml.inria.fr/svn/ocaml/trunk/Changes

Stéphane

PS:
btw, looks like coq is not really fond of this data type:

Inductive t a : Type :=
  | E : t a
  | D : t a -> t a -> t a
  | O : a -> t a
  | I : t (t a) -> t a
.

Error: Non strictly positive occurrence of "t" in "t (t a) -> t a".