fixes

LPCIC · Aug 20, 2021 · 281217e · 281217e
1 parent f7b242e
commit 281217e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git 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
@@ -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);