The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

That project seems to have branches for various Coq versions. In the 8.4 
branch that position in the failing file is not at the end of the proof, 
suggesting that the most recent version of the development is not 
compatible with 8.4.
Try the 8.4 branch or a newer Coq.

Gaëtan Gilbert

On 19/01/2018 19:51, Anthony Bordg wrote:
> Hi,
>
> I would like to build the coq package on projective geometry 
> <https://github.com/coq-contribs/projective-geometry> to go through the 
> proofs in the various files with Proof General or coqIDE. But using the 
> make command I got the following error:
>
>   File 
> "/home/anthony/projective-geometry/Plane/projective_plane_to_Heyting_projective_plane.v", 
> line 146, characters 0-4:
> Error: Attempt to save an incomplete proof
> Makefile.coq:245 : la recette pour la cible 
> « Plane/projective_plane_to_Heyting_projective_plane.vo » a échouée
> make[1]: *** [Plane/projective_plane_to_Heyting_projective_plane.vo] 
> Erreur 1
> make[1] : on quitte le répertoire « /home/anthony/projective-geometry »
> Makefile:2 : la recette pour la cible « all » a échouée
> make: *** [all] Erreur 2
>
> However, the aforementioned proof does not seem to be incomplete. I'm 
> using coq v.8.4pl4 on Ubuntu 16.04 LTS. Any help would be welcome.
>
> Regards
> Anthony
>
> --
> *PhD. Anthony Bordg
> *
> *Research Associate
> *
> *Cambridge University, UK
> https://sites.google.com/site/anthonybordg/*