Skip to content

Name conflict between theories/* and test/* in HoTT namespace #2313

@jdchristensen

Description

@jdchristensen

From HoTT Require Import Group. gives an error in recent Rocq versions because both HoTT and HoTT.Tests contain a file Group.v. We should separate these namespaces.

Metadata

Metadata

Assignees

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