Skip to content

Coq to Rocq name change #130

@PeterSewell

Description

@PeterSewell

Given the welcome name change of Coq to Rocq, we should add new homs. To preserve backwards compatability, the existing coq hom name should be retained, so we should just add a new synonym - either rocq or (to keep the three-letter-whenever-possible naming convention) roq. And similarly for the hom names that include coq as a substring. And the hom names like "ich" should have new synonyms like "ihr".

I don't think we should pervasively change instances of Coq inside the Ott source code (there are many, and I imagine that would be error-prone).

The tests that are used in the documentation (possibly all the simple tests) should be updated accordingly. Probably not the larger examples, though.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions