From 281217ea655ae68ef639765046d3334227585d9b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Aug 2021 15:45:40 +0200 Subject: [PATCH] fixes --- examples/tutorial_coq_elpi_HOAS.v | 2 +- examples/tutorial_style.rst | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/examples/tutorial_coq_elpi_HOAS.v b/examples/tutorial_coq_elpi_HOAS.v index 66938980b..80bee814d 100644 --- a/examples/tutorial_coq_elpi_HOAS.v +++ b/examples/tutorial_coq_elpi_HOAS.v @@ -459,7 +459,7 @@ Fail Elpi Query lp:{{ This fatal error says that `x` in `(Bo x)` is unknown to Coq. It is a variable postulated in Elpi, but it's type, `nat`, was lost. There -is nothing wrong per se in using `pi x\` as we did if we don't call Coq +is nothing wrong per se in using `pi x\ ` as we did if we don't call Coq APIs under it. But if we do, we have to record the type of `x` somewhere. In some sense Elpi's way of traversing a binder is similar to a Zipper. diff --git a/examples/tutorial_style.rst b/examples/tutorial_style.rst index 35b9749f7..8589849c7 100644 --- a/examples/tutorial_style.rst +++ b/examples/tutorial_style.rst @@ -84,6 +84,12 @@ font-feature-settings: "XV00" 1; /* Use Coq ligatures when Iosevka is available */ line-height: initial; } + + .highlight .-ElpiFunction { color: #795E26 } + .highlight .-ElpiVariable { color: #0000ff } + .highlight .k-ElpiKeyword { color: #AF00DB } + .highlight .k-ElpiMode { color: #811f3f } + .highlight .m-ElpiInteger { color: #098658 } `; document.getElementsByTagName('head')[0].appendChild(style);