update docs

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

encoding/README.adoc

+= 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

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.

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.