François Pottier

Thanks, I have removed these files. By the way (sorry if this is a bit off topic here), I see that many CI runs currently fail with `make: dune: No...

In principle I would be in favor of making `atomic` a keyword. I don't think an attribute should influence the semantics of the code. I would even go so far...

Sure, my comments about syntax were not meant to delay this PR. I just happen to think that syntax *is* an important aspect of language design, so I hope that...

Naive question: why is `Atomic.Loc.set` implemented in terms of `Atomic.Loc.exchange`? Isn't that needlessly costly?

Yes, the problem is fairly reproducible (stable). If I swap the order of the functions, the problem is the same. In fact, this is a simplified version of a problem...

Regarding allocation, you are correct, this benchmark does not allocate any memory. So, I guess you are right: `_caml_call_gc` is never called. Weird.

I have experimented with another loop, a small `blit` loop. It exhibits a similar phenomenon. This example is interesting, because + in OCaml 5, adding a type annotation makes the...

Hi Pierre-Marie! `nat` and `is_nat` are just examples here. In my actual real-world application, I have an abstract syntax tree `t` and a judgement `j` (say, a typing judgement, or...

Your comments regarding dependent types and intrinsically-typed representations suggest that there is a misunderstanding. I am using a plain (non-dependent) type of terms and defining a well-typedness judgement on the...

Of course, in this example, the typing judgement `wt` is true of every term, so one can prove `forall t, wt t` and be done with it. But in real-world...