Skip to content

Commit

Permalink
small typo
Browse files Browse the repository at this point in the history
  • Loading branch information
@patrick-nicodemus
patrick-nicodemus authored Jan 30, 2025
1 parent 83aaada commit 9761bf4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion builtin-doc/coq-builtin.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1458,7 +1458,7 @@ external pred coq.unify-eq i:term, i:term, o:diagnostic.
% if they are types)
external pred coq.unify-leq i:term, i:term, o:diagnostic.

% [coq.elaborate-skeleton T ETy E Diagnostic] elabotares T against the
% [coq.elaborate-skeleton T ETy E Diagnostic] elaborates T against the
% expected type ETy.
% T is allowed to contain holes (unification variables) but these are
% not assigned even if the elaborated term has a term in place of the
Expand Down

0 comments on commit 9761bf4

Please sign in to comment.