search

math-comp / math-comp

Mathematical Components
https://math-comp.github.io
589 stars 115 forks source link

Document global flags set by mathcomp #1262

Open KimayaBedarkar opened 3 months ago

KimayaBedarkar commented 3 months ago

Mathcomp changes some default coq behaviors globally by setting some flags. Examples: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssreflect.v#L5-L6 These global behaviors are inherited by any project that imports mathcomp. So, these flags having global effects should all be set in one file and explicitly documented.

proux01 commented 3 months ago

Mathcomp changes some default coq behaviors globally by setting some flags. Examples: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssreflect.v#L5-L6 These global behaviors are inherited by any project that imports mathcomp. So, these flags having global effects should all be set in one file

Isn't it already the case with ssreflect.v?

and explicitly documented.

Indeed, there should be a header comment at the beginning of ssreflect.v telling to go look at ssreflect.v in Coq and the few global flags (then telling to look below for more recent changes).