Roland Zumkeller wrote:
> On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
>> The fact that something is well-typed in Coq does not mean that you can
>> just translate it to OCaml by adding a few Obj.magic to make the
>> type-checker happy.
> 
> As I understand Pierre Letouzey's PhD thesis explains how this can be
> done. Your example couldn't result from translating a Coq term, since
> "String.copy", "ref", and "Gc.major" are not part of its formalism (a
> flavour of lambda calculus with inductive types).

Here is an example which might fall into this class:

let f n =
  let x = if ("a" = "b") then Obj.magic 0 else (Some n) in
  for i = 0 to 100000 do ignore (Some i) done;
  (match x with Some n -> print_int n | None -> ());
in
f 10

It prints 512 on my machine (when compiled with ocamlopt).

> On my machine it prints "$d$d$d$d$d$d$d$d$d$d$d$d$d$d$d" and when
> compiled with ocamlc "abc". Is this a bug?

No, undefined behaviors are not specified.

-- Alain