Skip to content

Commit

Permalink
Change wording in documentation
Browse files Browse the repository at this point in the history
I think that this is supposed to say the opposite of what it says. I tested it to confirm - by default, `elaborate-skeleton` does infer typeclasses, and with `@no-tc!` it does not.
  • Loading branch information
patrick-nicodemus authored Jan 30, 2025
1 parent 83aaada commit ce43486
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion builtin-doc/coq-builtin.elpi
Original file line number Diff line number Diff line change
Expand Up @@ -1465,7 +1465,7 @@ external pred coq.unify-leq i:term, i:term, o:diagnostic.
% hole. Similarly universe levels present in T are disregarded.
% Supported attributes:
% - @keepunivs! (default false, do not disregard universe levels)
% - @no-tc! (default false, do not infer typeclasses)
% - @no-tc! (default false, do infer typeclasses)
external pred coq.elaborate-skeleton i:term, o:term, o:term, o:diagnostic.

% [coq.elaborate-ty-skeleton T U E Diagnostic] elabotares T expecting it to
Expand Down

0 comments on commit ce43486

Please sign in to comment.