From 4603ea301f4feaf8bb414065af317ae6b59ef0e8 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 15 Oct 2024 17:08:50 +0200 Subject: [PATCH] Small typo in documentation --- examples/tutorial_coq_elpi_HOAS.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 8ce682784..4bc248b14 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -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