diff --git a/src/Addressing.v b/src/Addressing.v
index 754a02f..acd100f 100644
--- a/src/Addressing.v
+++ b/src/Addressing.v
@@ -134,6 +134,21 @@ and memory locations.
      ```
      add 42, r0, r3
      ```
+
+     Note that negative imm operands may be supported by the assembler, for example:
+
+     ```
+     add -42, r0, r3
+     ```
+
+However, the implementation will have to proceed as follows:
+
+- put a negative immediate `-42` on a const page to an address $C$, as a 2's complement, 256-bit wide;
+- using the [%const_in] addessing mode, address the $C$-th constant, as in the following pseudocode:
+
+```
+add code[C], r0, r3
+```
    *)
 
   Inductive imm_in : Type := Imm (imm: u16).
diff --git a/src/Introduction.v b/src/Introduction.v
index 5073481..a53ba44 100644
--- a/src/Introduction.v
+++ b/src/Introduction.v
@@ -135,5 +135,5 @@ instruction syntax and semantics, and some elements of system protocol.
   + [%Bootloader] : a system contract in charge of block construction.
   + [%Precompiles] : extensions of virtual machine.
   + [%VersionedHash] : used to fetch the contract code.
-  + [%Decommitter]
+  + [%Decommitter] : fetches the contract code.
  *)
diff --git a/src/encoding/EncodingUtils.v b/src/encoding/EncodingUtils.v
index 0f8b3fb..670e06f 100644
--- a/src/encoding/EncodingUtils.v
+++ b/src/encoding/EncodingUtils.v
@@ -81,7 +81,7 @@ Definition encode_swap(m: mod_swap) : Z :=
   end
 .
 
-(** 2. [encode_predicate] maps eight different predicates to their encodings as 3-bit
+(** 2. [%encode_predicate] maps eight different predicates to their encodings as 3-bit
   binary numbers.
 *)
 Definition encode_predicate (p:predicate) : BITS 3 :=
diff --git a/src/isa/CoreSet.v b/src/isa/CoreSet.v
index 1b5e230..c0adfce 100644
--- a/src/isa/CoreSet.v
+++ b/src/isa/CoreSet.v
@@ -9,7 +9,7 @@ The meaning of "schema" here is that [%instruction] needs to be specialized with
 a proper instance of [%descr] record to describe an instruction at different
 stages of its execution.
 
-The schema [instruction] is parameterized with types of various instruction operands.
+The schema [%instruction] is parameterized with types of various instruction operands.
 Conventionally, their names reflect the following information:
 
 - the prefix is `src_` for source operands and `dest_` for output operands.
diff --git a/src/isa/Instructions.v b/src/isa/Instructions.v
index 327ca15..90dae29 100644
--- a/src/isa/Instructions.v
+++ b/src/isa/Instructions.v
@@ -8,7 +8,7 @@ Section InstructionSets.
 The spec introduces the following layers of abstraction for the instruction set,
 from lowest level to the highest level:
 
-1. Binary encoding (as [BITS 64] type instances).
+1. Binary encoding (as [%BITS 64] type instances).
    Binary encoded instructions, each instruction is 64-bit wide.
 
    The exact type for such instructions is [%BITS 64].
diff --git a/src/sem/Farcall.v b/src/sem/Farcall.v
index 3408e39..4a170f9 100644
--- a/src/sem/Farcall.v
+++ b/src/sem/Farcall.v
@@ -227,30 +227,30 @@ A system call is a far call that satisfies the following conditions:
 ## Abstract and concrete syntax
 
 - [%OpFarCall] `abi_params address handler is_static `
-   + `farcall        abi_reg, dest_addr`
-   + `farcall        abi_reg, dest_addr, handler `
-   + `farcall.static abi_reg, dest_addr`
-   + `farcall.static abi_reg, dest_addr, handler`
-   + `farcall.shard  abi_reg, dest_addr`
-   + `farcall.shard  abi_reg, dest_addr, handler`
+   + `far_call        abi_reg, dest_addr`
+   + `far_call        abi_reg, dest_addr, handler `
+   + `far_call.static abi_reg, dest_addr`
+   + `far_call.static abi_reg, dest_addr, handler`
+   + `far_call.shard  abi_reg, dest_addr`
+   + `far_call.shard  abi_reg, dest_addr, handler`
 
 
 - [%OpDelegateCall] abi_params address handler is_static`
-   + `delegatecall        abi_reg, dest_addr`
-   + `delegatecall        abi_reg, dest_addr, handler`
-   + `delegatecall.static abi_reg, dest_addr`
-   + `delegatecall.static abi_reg, dest_addr, handler`
-   + `delegatecall.shard  abi_reg, dest_addr`
-   + `delegatecall.shard  abi_reg, dest_addr, handler`
+   + `far_call.delegate        abi_reg, dest_addr`
+   + `far_call.delegate        abi_reg, dest_addr, handler`
+   + `far_call.delegate.static abi_reg, dest_addr`
+   + `far_call.delegate.static abi_reg, dest_addr, handler`
+   + `far_call.delegate.shard  abi_reg, dest_addr`
+   + `far_call.delegate.shard  abi_reg, dest_addr, handler`
 
 
 - [%OpMimicCall] `abi_params address handler is_static`
-   + `mimic        abi_reg, dest_addr`
-   + `mimic        abi_reg, dest_addr, handler`
-   + `mimic.static abi_reg, dest_addr`
-   + `mimic.static abi_reg, dest_addr, handler`
-   + `mimic.shard  abi_reg, dest_addr`
-   + `mimic.shard  abi_reg, dest_addr, handler`
+   + `far_call.mimic        abi_reg, dest_addr`
+   + `far_call.mimic        abi_reg, dest_addr, handler`
+   + `far_call.mimic.static abi_reg, dest_addr`
+   + `far_call.mimic.static abi_reg, dest_addr, handler`
+   + `far_call.mimic.shard  abi_reg, dest_addr`
+   + `far_call.mimic.shard  abi_reg, dest_addr, handler`
 
 
 - **static** modifier marks the new execution stack frame as 'static', preventing some instructions from being executed.