diff --git a/README.md b/README.md
index ac05d9bbe583e8f9d6d9591813e5f81b5af8738a..6dec03fa4ac635ba29a1835e468a7be3d4dab538 100644
--- a/README.md
+++ b/README.md
@@ -13,14 +13,22 @@ library, also known as _Prelude_. The prelude is available
 
 
 ## Requirements
+
 [`lambdapi`](https://github.com/Deducteam/lambdapi.git) later than 
 fda8752584af52cdc8158a7a80bbe7fce5720616
 
 ## Structure
-- `adlib` contains additional libraries not in the prelude
-- `encodings` contains encodings of PVS into Dedukti, most of the work is done
-  using `cert_f` encoding
-- `prelude` contains parts of the PVS prelude
-- `sandbox` contains miscellaneous experiments
-- `tools` contains some additional scripts and utilities
-- `alternatives` contains files in other encodings
+
+- `adlib`: additional libraries not in the prelude
+- `encodings`: encoding of PVS into Dedukti
+- `prelude`: parts of the PVS prelude
+- `sandbox`: miscellaneous experiments
+- `tools`: some additional scripts and utilities
+
+## Dedukti coding conventions
+
+- Dedukti types are capitalised  
+  `Nat: TYPE`
+- Predicates are suffixed with `_p`  
+  `even_p: Nat → Bool`
+- Documentation is commented with `///`
diff --git a/encodings/deptype.lp b/encodings/deptype.lp
index 60b1624dfb30160e70cb8fbcadf4b4d965707ea8..cb2e340d28322eea9c1c485d5e87c52426a8a181 100644
--- a/encodings/deptype.lp
+++ b/encodings/deptype.lp
@@ -1,8 +1,10 @@
 /// Dependent types
+
 /// PVS allows dependent types using theory abstraction. For instance,
 /// vector[t: TYPE, n: nat]: THEORY BEGIN vec: TYPE END vector
 /// allows to define
 /// cons(n: nat, e: t, v: vector[t, n].vec): vector[t, n + 1].vec
+
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 0fc57f84177b955cc41e09c9a3b31b93710e0a80..7418cef5bd1dad41b1a1bb74acffbbb0e68e7730 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -1,4 +1,4 @@
-// Encoding of λHOL
+/// Encoding of λHOL
 symbol Kind: TYPE
 symbol Set: TYPE
 symbol Bool: TYPE
diff --git a/encodings/prenex.lp b/encodings/prenex.lp
index e2b4901cfe57eca93bcf3c5086cb2df2c17b3a8a..4bd990b0bf41fe3d9b685e04ed3ef7c5b5a1fbae 100644
--- a/encodings/prenex.lp
+++ b/encodings/prenex.lp
@@ -1,4 +1,10 @@
-// Prenex polymorphism: prenex quantification on elements of type ‘Set’.
+/// Prenex polymorphism
+
+/// Prenex polymorphism allows to quantify over variables of type ‘Set’.
+/// PVS allows it in theory formals, such as
+/// groups[t: TYPE]: THEORY BEGIN ... END groups
+/// For more informations on the encoding of prenex polymorphism, see
+/// https://arxiv.org/abs/1807.01873 and theory U
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
@@ -11,17 +17,17 @@ set declared "∀S"
 // Quantification for objects of type ‘Bool’
 set declared "∀B"
 
-symbol SchemeK: TYPE
+constant symbol SchemeK: TYPE
 symbol ϕ: SchemeK → TYPE
-symbol scheme_k: Kind → SchemeK
+constant symbol scheme_k: Kind → SchemeK
 rule ϕ (scheme_k $X) ↪ θ $X
 
 constant symbol ∀K: (Set → SchemeK) → SchemeK
 rule ϕ (∀K $e) ↪ Πt: Set, ϕ ($e t)
 
-symbol SchemeS: TYPE
+constant symbol SchemeS: TYPE
 symbol χ: SchemeS → TYPE
-symbol scheme_s: Set → SchemeS
+constant symbol scheme_s: Set → SchemeS
 rule χ (scheme_s $X) ↪ η $X
 
 constant symbol ∀S: (Set → SchemeS) → SchemeS