I am porting a library from an older version of Coq to coq 8.12.1 and can't get (Ocaml) extraction to work properly.

There are three definitions of the `int`

type: in `Numeral.ml`

, `Hexadecimal.ml`

, and `Decimal.ml`

, none of which are compatible with ocaml's `int`

(which is what I expect/want). This breaks the ocaml glue code that calls it.

Any ideas on how to solve this?

This did not happen with older versions of Coq.

The extraction file is using

```
Require Import ExtrOcamlBasic ExtrOcamlString ExtrOcamlNatInt ExtrOcamlZInt.
```

The full Coq file used for extraction is available here: https://github.com/IBM/FormalML/blob/coq8.12/ocaml/NnoptExtraction.v

I have not been able to figure out why it is not working anymore. Any ideas?

That's a known issue. Extraction handles badly this case, and the current workarounds are discussed here: https://github.com/coq/coq/issues/13288

We will hopefully have a solution by 8.13 :fingers_crossed:

Matthieu Sozeau said:

That's a known issue. Extraction handles badly this case, and the current workarounds are discussed here: https://github.com/coq/coq/issues/13288

Thanks! the workaround suggested in the issue linked from that issue resolves the problem and allows extraction to work again.

Last updated: May 18 2024 at 08:40 UTC