From 7c7abade2c51babcfc4e4a9b65896930406611d5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 8 Dec 2023 11:29:14 +0100 Subject: [PATCH 1/3] Update tutorial_coq_elpi_command.v --- examples/tutorial_coq_elpi_command.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index caaf5e68f..cd3722ad2 100644 --- a/examples/tutorial_coq_elpi_command.v +++ b/examples/tutorial_coq_elpi_command.v @@ -617,7 +617,7 @@ the string :e:`"33"`. Attributes are usually validated (parsed) and turned into regular options using :lib-common:`coq.parse-attributes` and a description of their types using -the :libtype:`attribute-type` data type: +the :lib-common:`attribute-type` data type: |*) From 46a841248645e427f433693d3d332848e05a7053 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 8 Dec 2023 12:11:18 +0100 Subject: [PATCH 2/3] Update tutorial_style.rst --- etc/tutorial_style.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/etc/tutorial_style.rst b/etc/tutorial_style.rst index f93383e3c..7740c7d17 100644 --- a/etc/tutorial_style.rst +++ b/etc/tutorial_style.rst @@ -40,6 +40,9 @@ .. role:: libtype(elpi-type) :src: LPCIC coq-elpi master elpi/coq-lib.elpi +.. role:: libtype-common(elpi-type) + :src: LPCIC coq-elpi master elpi/coq-lib-common.elpi + .. role:: stdtype(elpi-type) :src: LPCIC coq-elpi master elpi-builtin.elpi From c8848b64420cf8e9582e05d5efefab6dd76f7108 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 8 Dec 2023 12:11:29 +0100 Subject: [PATCH 3/3] Update examples/tutorial_coq_elpi_command.v --- examples/tutorial_coq_elpi_command.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index cd3722ad2..42256a037 100644 --- a/examples/tutorial_coq_elpi_command.v +++ b/examples/tutorial_coq_elpi_command.v @@ -617,7 +617,7 @@ the string :e:`"33"`. Attributes are usually validated (parsed) and turned into regular options using :lib-common:`coq.parse-attributes` and a description of their types using -the :lib-common:`attribute-type` data type: +the :libtype-common:`attribute-type` data type: |*)