Skip to content

Commit

Permalink
Merge pull request #701 from ckeller/doc-typo
Browse files Browse the repository at this point in the history
Small typo in documentation
  • Loading branch information
gares authored Oct 16, 2024
2 parents c7174ba + 4603ea3 commit 4b55e8e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion examples/tutorial_coq_elpi_HOAS.v
Original file line number Diff line number Diff line change
Expand Up @@ -656,7 +656,7 @@ Outside the pattern fragment
This encoding of evars is such that the programmer does not need to care
much about them: no need to carry around an assignment/typing map like the
Evar map, no need to declared new variables there, etc. The programmer
Evar map, no need to declare new variables there, etc. The programmer
can freely call Coq API passing an Elpi term containing holes.
There is one limitation, though. The rest of this tutorial describes it
Expand Down

0 comments on commit 4b55e8e

Please sign in to comment.