Compile Before Require not working anymore

[viampietro]

Hello everyone,

I'm using emacs 25.2.2 with company-coq 20200729.401 (installed through melpa).
When I enable the "Compile Before Require" option in the menu bar and I hit "C-c Enter" to get all my required libraries compiled, then company-coq stalls at the first "Require Import" line.

In the Messages buffer, it says:

Unexpected error during parallel compilation: (wrong-number-of-arguments (1 . 3) 4)
proof-extend-queue: Wrong number of arguments: (1 . 3), 4

I don't if it comes from my set up (maybe my Emacs version is too old) or from company-coq.

Thanks,

Vincent

[viampietro]

I forgot to mention that I am using Coq version 8.12

[cpitclaudel]

I think this is a bug in Proof General (not company-coq), probably related to recent changes in compile before require. Maybe ProofGeneral/PG#523 ?