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 diff --git a/examples/tutorial_coq_elpi_command.v b/examples/tutorial_coq_elpi_command.v index caaf5e68f..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 :libtype:`attribute-type` data type: +the :libtype-common:`attribute-type` data type: |*)