From d022bfdbcc023278faeb8e708171daecac4d7dfb Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabriel@motacilla.home>
Date: Sun, 24 Oct 2021 10:40:48 +0200
Subject: [PATCH] update docs

---
 docs/main.adoc                | 36 ++++-------------------------------
 encoding/README.adoc          | 27 ++++++++++++++++++++++++++
 specs/tools/README.md         |  3 ++-
 specs/tools/prelude/README.md |  6 +++---
 4 files changed, 36 insertions(+), 36 deletions(-)
 create mode 100644 encoding/README.adoc

diff --git a/docs/main.adoc b/docs/main.adoc
index 6a321dd..77f4a00 100644
--- a/docs/main.adoc
+++ b/docs/main.adoc
@@ -168,9 +168,12 @@ the variable +$PERSONOJPATH+.
 
 === Translating the Prelude ===
 
+CAUTION: BSD makefiles are used rather than GNU makefiles. Linux users
+may have to use +bmake+ rather than +make+.
+
 [source,sh]
 cd specs/tools/prelude
-bmake
+make
 
 will create a set of empty +.lp+ files and translate and type check
 other files. The (nearly) empty files stand for theories that can't be
@@ -178,34 +181,3 @@ translated yet.
 
 TIP: if the translation fails, ensure that +$PVSPATH+ and
 +$PERSONOJPATH+ are correctly set up.
-
-== Implementation details ==
-
-=== Encoding ===
-
-The encoding is a set of lambdapi files in +encoding/+ that define
-axioms allowing to type check PVS terms and propositions.
-
-+lhol.lp+ ::
-  Simple Type theory expressed as a PTS commonly named λHOL
-+pvs_cert.lp+ ::
-  Explicit predicate subtyping
-+tuple.lp+ ::
-  Non dependents tuples. Can also be seen as a non dependent version
-  of link:https://doi.org/10.1016/0890-5401(91)90066-B[de Bruijn
-  telescopes].
-+logical.lp+ ::
-  Locical connectives
-+eqtup.lp+ ::
-  Uncurried equality and disequality, latexmath:[$eq (t, u)$]
-+coercions.lp+ ::
-  Define coercions to implement implicit predicate subtyping
-+extra+ ::
-  More definitions and tools
-  +arity-tools.lp+ :::
-    An encoding of natural numbers used in data structures (they are
-    not the natural numbers used in PVS)
-+alt+ ::
-  Alternate definitions
-+examples+ ::
-  Some example specification
diff --git a/encoding/README.adoc b/encoding/README.adoc
new file mode 100644
index 0000000..c6b4cbf
--- /dev/null
+++ b/encoding/README.adoc
@@ -0,0 +1,27 @@
+= Encodings =
+Gabriel Hondet <gabriel.hondet@inria.fr>
+v1.0, October 2021
+
+The encoding is a set of lambdapi files in +encoding/+ that define
+axioms allowing to type check PVS terms and propositions.
+
+lhol ::
+  Simple Type theory expressed as a PTS commonly named λHOL
+pvs_cert ::
+  Explicit predicate subtyping
+tuple ::
+  Non dependents, lengthed tuples. Can also be seen as a non dependent
+  version of link:https://doi.org/10.1016/0890-5401(91)90066-B[de
+  Bruijn telescopes].
+logical ::
+  Locical connectives
+eqtup ::
+  Uncurried equality and disequality, latexmath:[$eq (t, u)$]
+coercions ::
+  Define coercions to implement implicit predicate subtyping
+extra ::
+  More definitions and tools
+alt ::
+  Alternate definitions
+examples ::
+  Some example specification
diff --git a/specs/tools/README.md b/specs/tools/README.md
index f5913f3..ff257bf 100644
--- a/specs/tools/README.md
+++ b/specs/tools/README.md
@@ -7,4 +7,5 @@ to Dedukti files.
 - `pvs2dk.sh`: translate a theory to a lambdapi file.
 - `lambdapi.pkg`: the module file for lambdapi (required to type check files).
 - `lambdapi.mk`: some targets and rules to typecheck lambdapi files.
-- `*.patch`: patches that may be apply to the Prelude to translate it.
+- `prelude_patches/*.diff`: patches that may be apply to the Prelude to
+	translate it.
diff --git a/specs/tools/prelude/README.md b/specs/tools/prelude/README.md
index 34da6d7..1afc718 100644
--- a/specs/tools/prelude/README.md
+++ b/specs/tools/prelude/README.md
@@ -25,9 +25,9 @@ make functions.lpo
 
 The theories of the Prelude are registered in the file `theories`. In this file,
 each line is a theory. One-line comments can be inserted with character `#` *at
-the beginning of the file*.
+the beginning of the line*.
 If a theory name is prefixed with a dash `-`, the theory is not translated nor
-type-checked. Instead, an empty file can be created with the name of the theory
-using `mk_dummy.sh`.  This allows to translate and type check theories that are
+type-checked. Instead, an empty file is created with the name of the theory by
+`mk_dummy.sh`.  This allows to translate and type check theories that are
 defined further in the prelude, but do not depend on them, as theories of
 prelude require (syntactically) all previous prelude theories.
-- 
GitLab