search

Lysxia / coq-ceres

Coq library for serialization to S-expressions
MIT License
18 stars 1 forks source link

Prefix all modules with Ceres #10

Closed Lysxia closed 5 years ago

Lysxia commented 5 years ago

Format and String are OCaml standard library modules, and the other modules have generic enough names that they are bound to cause issues too.

Ideally the Extraction plugin should use the full logical path to produce the module name, so theories/String.v extracts to Ceres__String for instance. But for backwards compatibility, we're stuck with this kind of manual mangling.

Ping @liyishuai @YaZKo so you know it's coming.

YaZko commented 5 years ago

That sounds great, thanks for the change! And I actually prefer this heavy-handed change that a hack into extraction since the names also clash with Coq's standard library. In particular it shadows Coq's String.