Sorry it has been a long time since I last compiled by myself with ocamlc. Indeed, your solution worked but, with ocamlc, there is a need to add the -I option so that it knows what directory it should use. The line is now:
CWCompileAndRun "fibo.mli" "fibo.ml" Options "-I /opt/coq/default/lib/num /opt/coq/default/lib/num/nums.cma -w -8" Driver "

Honestly, in my opinion, it is almost always simpler to use modern tools like opam/dune when working with OCaml. I guess you were not able to do that because Opam is broken on Debian stable (I don't know it it is still broken actually ?).
Anyway, thank you for your help.
I republished and marked this issue as solved.

I managed to make the Coq proof ok (not deployed) for now but I still get some OCaml error. It seems that the nums.cma file is not available:

File "fibo.ml", line 16, characters 16-31:
16 |   type coq_Ze = Big_int.big_int
                     ^^^^^^^^^^^^^^^
Error: Unbound module Big_int
Running: ocamlc nums.cma -w -8 fibo.ml driver.ml

I think maybe it is necessary to install the library num for this new ocamlc ? I hope it could be handled by this command (if you use opam the package manager of ocaml):
opam install num

Most likely, this comes from the way my solution is written (the behavior of some tactics changed between 8.11 and 8.12): I can modify this when I have time.
Thank you for your help.

I looked it up a little bit. There seems to be a problem with the CWCompileAndRun command with Coq8.12. I get the following error: "ocamlc not found".
The test for the plugin in coq_codewars repository (coq plugin) seems to still be working well with Coq 8.12.
I cannot solve this CWCompileAndRun problem on my own (but I can help by providing a solution compatible with Coq 8.12).

I agree with the statement of ipergenitsa above. Perhaps, for Coq and other theorem proving tools, it would be a good idea to differentiate between different aspects of the katas complexity (with a tag ?):

• Program and prove: the main difficulty is to write and prove a program
• Mathematics: the main difficulty is to find the proof in theoretical maths (I mean that translating it into Coq is easy but the reasonning is hard)
• Logicians and tricks of Coq: the main difficulty is to know the very last features of the tool and the exact logic it relies on.

I think this particular problem would fall into the second category meaning that it is significantly harder for someone with a small background in mathematics. I personally struggled with problems of the third category (for example one using the very new feature of polymorphic universes in Coq).
Note that I may have missed the relevant tags and the respective meaning of 8kyu/7kyu etc (pointers are welcome ;) )

I submitted a solution with Coq8.11 and republished. I guess there is only that to do. So, it should be working now.

Should be solved now.

Done.

Indeed, it makes more sense with this operation: I forgot it.

I added an extraction test using CWCompileAndRun as suggested. Is there a way to test that the solution you proposed is correctly removed ? Should I republish this kata ?

I see. I think it may be difficult to edit the Coq plugin. I may open an issue for this in the future (when I have time).

Thanks for the advice, the kata is unpublished.