Skip to content

Commit 49f8618

Browse files
Merge pull request #240 from SkyLabsAI/gmalecha/dependent-name-printer
Bug fixes for dependent name printer
2 parents 6a6ca39 + 0515022 commit 49f8618

16 files changed

Lines changed: 1180 additions & 252 deletions

File tree

rocq-skylabs-brick/AGENTS.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
# AGENTS.md
2+
3+
- In Rocq tests that mention C++ names or types, prefer the string notations
4+
such as `%cpp_name` and `%cpp_type` when they can express the expected term.
5+
Use explicit constructors only for cases the notation cannot represent, such
6+
as template-template parameter variables (`Atemplate_param`).

0 commit comments

Comments
 (0)