From 2ed2fb3fe9a396530fa211584e0658b8cf805787 Mon Sep 17 00:00:00 2001 From: lapinot Date: Thu, 30 May 2024 21:36:16 +0200 Subject: [PATCH] typos --- theories/OGS/Soundness.v | 2 +- theories/Readme.v | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/OGS/Soundness.v b/theories/OGS/Soundness.v index a0c9ee7..b3b5d89 100644 --- a/theories/OGS/Soundness.v +++ b/theories/OGS/Soundness.v @@ -89,5 +89,5 @@ to provide with several examples: The second command will explicit if any axiom has been used to establish the result. As stated in the `prelude `_, we exclusively use -:coqid:`Coq.Eqdep.Eq_rect_eq.eq_rect_eq`, ie Streicher's axiom K. +:coqid:`Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq`, ie Streicher's axiom K. |*) diff --git a/theories/Readme.v b/theories/Readme.v index 7cdda8e..418ff50 100644 --- a/theories/Readme.v +++ b/theories/Readme.v @@ -61,7 +61,7 @@ or manually: Building the project ^^^^^^^^^^^^^^^^^^^^ -... code:: shell +.. code:: shell dune build @@ -75,7 +75,7 @@ To build the html documentation, first install Alectryon: opam install "coq-serapi==8.17.0+0.17.1" python3 -m pip install --user alectryon -The build with: +Then build with: .. code:: shell @@ -150,7 +150,7 @@ Axioms ^^^^^^ The whole development relies only on axiom K, a conventional and sound axiom -from Coq's standard library (more precisely, :coqid:`Coq.Eqdep.Eq_rect_eq.eq_rect_eq`). +from Coq's standard library (more precisely, :coqid:`Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq`). This can be double checked as follows: