[core] [api] Rename Int and Option modules.

[ejgallego]

OCaml 4.08.0 has introduced Int and Option modules, we thus rename
Coq's to CInt and COption to avoid problems with upstream.

[SkySkimmer]

This is the Int module of ltac2, it hasn't changed name Gaëtan Gilbert

…

On 09/07/2019 15:55, Emilio Jesús Gallego Arias wrote: ***@***.**** commented on this pull request. ------------------------------------------------------------------------ In test-suite/ltac2/errors.v <#10469 (comment)>: > @@ -5,7 +5,7 @@ Proof. let x := Control.plus (fun () => let _ := constr:(nat -> 0) in 0) (fun e => match e with Not_found => 1 | _ => 2 end) in -match Int.equal x 2 with +match CInt.equal x 2 with Why? — You are receiving this because your review was requested. Reply to this email directly, view it on GitHub <#10469?email_source=notifications&email_token=AASZB3EKAQSGISDUWOQZFTDP6SKFFA5CNFSM4H5A5T22YY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOB5364DI#discussion_r301599839>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AASZB3H7I6FQQBKEED7FC5DP6SKFFANCNFSM4H5A5T2Q>.

[SkySkimmer]

So are we doing this or not?

[ejgallego]

So are we doing this or not?

Main motivation for me to do this is ocaml/merlin#1003 , but I'm unsure about what the right behavior is here and I didn't have to time to look into it too much, so kinda waiting for the merlin people to comment.

[XVilka]

There are many conflicts now.

[ejgallego]

Rebasing is trivial, but before doing it; I wonder: what should we do with this PR?

The PR is targeted at 8.11 beta, I dunno what to do, we never set a formal policy about this, but it has been the norm in the past than whenever OCaml does introduce some new modules we rename our conflicting ones. [we should be able to stop doing this once we can pack our modules]

[ppedrot]

Judging from the lack of reaction I propose postponing to 8.12.

[ejgallego]

Judging from the lack of reaction I propose postponing to 8.12.

I guess we can just close this if we don't merge; I don't see the point on having this on 8.12 but not on 8.11. On the other hand we should check we are not having any double linking in 4.08.0 / 4.09.0 [unsure because of the upstream packing]

If that's the case this patch must land in 8.11

[ejgallego]

On the other hand we should check we are not having any double linking in 4.08.0 / 4.09.0 [unsure because of the upstream packing]

If that's the case this patch must land in 8.11

After some checking things seem to be fine; so this patch is not a must.

On the other hand it may be desirable for other reasons, for example merlin has a bug that will get it confused without this patch [1], so I did a last rebase just in case we want to ship it in the last minute.

[1] ocaml/merlin#1003

[ejgallego]

In the end we have decided that this is overkill, as the upstream modules are already packed.