We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The _CoqProject file currently has this line:
_CoqProject
-R theories HighSchoolGeometry
According to best practices, it should be ensured that the project builds with the -Q option instead of only -R (see documentation for coqc).
-Q
-R
coqc
To accomplish this, all unqualified Require Import must be replaced with qualified versions. For example, this line
Require Import
Require Export Plans_paralleles.
needs to be replaced with
From HighSchoolGeometry Require Export Plans_paralleles.
cc: @jp-diegidio
The text was updated successfully, but these errors were encountered:
jp-diegidio
Successfully merging a pull request may close this issue.
The
_CoqProject
file currently has this line:According to best practices, it should be ensured that the project builds with the
-Q
option instead of only-R
(see documentation forcoqc
).To accomplish this, all unqualified
Require Import
must be replaced with qualified versions. For example, this lineneeds to be replaced with
cc: @jp-diegidio
The text was updated successfully, but these errors were encountered: