diff --git a/src/parser/pascaligo/Doc/pascaligo.txt b/src/parser/pascaligo/Doc/pascaligo.txt
index 5b6b78696..53c4d79fc 100644
--- a/src/parser/pascaligo/Doc/pascaligo.txt
+++ b/src/parser/pascaligo/Doc/pascaligo.txt
@@ -190,15 +190,15 @@ the latter can be reassigned. The syntax is slightly different for
 both. For example, the variables "x" and "y" above could have been
 declared as follows:
 
-var x : nat := 0;
-var y : nat := 0;
+var x : nat := 0n;
+var y : nat := 0n;
 
 It is possible to specify that the value of a variable will not change
 (the name "variable" is misleading in that context), that is, they
 remain constant:
 
-const ten : nat = 10;
-const eleven : nat = ten + 1;
+const ten : nat = 10n;
+const eleven : nat = ten + 1n;
 
 Similarly, function declarations have their parameters and return
 value annotated with their types. For instance,
@@ -214,10 +214,10 @@ the result of calling the function is given after the keyword "with".
 A another example would be
 
 function factorial (const n : nat) : nat is
-  var m : nat := 0;
-  var f : nat := 1;
+  var m : nat := 0n;
+  var f : nat := 1n;
   begin
-    if n <= 0 then f := 1
+    if n <= 0n then f := 1n
     else
       for m := 1 to n
         begin
diff --git a/src/parser/pascaligo/Doc/pascaligo_21.bnf b/src/parser/pascaligo/Doc/pascaligo_21.bnf
new file mode 100644
index 000000000..d99ef835b
--- /dev/null
+++ b/src/parser/pascaligo/Doc/pascaligo_21.bnf
@@ -0,0 +1,375 @@
+right_assoc(item,op) ::=
+  item
+| item op right_assoc(item,op)
+
+left_assoc(item,op) ::=
+  right_assoc(item,op)
+
+option(item) :=
+  (**)
+| item
+
+series(item,sep,term) ::=
+  item after_item(item,sep,term)
+
+after_item(item,sep,term) ::=
+  sep item_or_closing(item,sep,term)
+| term
+
+item_or_closing(item,sep,term) ::=
+  term
+| series(item,sep,term)
+
+(* Compound constructs *)
+
+par(item) ::=
+  LPAR item RPAR
+
+brackets(item) ::=
+  LBRACKET item RBRACKET
+
+(* Sequences *)
+
+(* Possibly empty sequence of items *)
+
+seq(item) ::=
+  option(nseq(item))
+
+(* Non-empty sequence of items *)
+
+nseq(item) ::=
+  item seq(item)
+
+(* Non-empty separated sequence of items *)
+
+nsepseq(item,Sep) ::=
+  item
+| item Sep nsepseq(item,Sep)
+
+(* Possibly empty separated sequence of items *)
+
+sepseq(item,Sep) ::=
+  option(nsepseq(item,Sep))
+
+(* Main *)
+
+contract ::=
+  nseq(declaration) EOF
+
+declaration ::=
+  type_decl   option(SEMI)
+| const_decl  option(SEMI)
+| lambda_decl option(SEMI)
+
+(* Type declarations *)
+
+type_decl ::=
+  Type Ident Is type_expr
+
+type_expr ::=
+  cartesian
+| nsepseq(variant,VBAR)
+| VBAR nsepseq(variant,VBAR)
+| Record record_type_expr
+
+record_type_expr ::=
+  series(field_decl,SEMI,End)
+| LBRACKET series(field_decl,SEMI,RBRACKET)
+
+variant ::=
+  Constr option(of_cartesian)
+
+of_cartesian ::=
+  Of cartesian
+
+cartesian ::=
+  nsepseq(function_type,TIMES)
+
+function_type ::=
+  right_assoc(core_type,ARROW)
+
+core_type ::=
+  Ident (* type_name *) option(type_tuple)
+| Map type_tuple
+| Set par(type_expr)
+| List par(type_expr)
+| par(type_expr)
+
+type_tuple ::=
+  par(nsepseq(type_expr,COMMA))
+
+field_decl ::=
+  Ident (* field_name *) COLON type_expr
+
+(* Function and procedure declarations *)
+
+lambda_decl ::=
+  fun_decl
+| proc_decl
+| entry_decl
+
+fun_decl ::=
+  Function Ident parameters COLON type_expr Is
+    seq(local_decl)
+    block
+  With expr
+
+entry_decl ::=
+  Entrypoint Ident entry_params COLON type_expr Is
+    seq(local_decl)
+    block
+  With expr
+
+entry_params ::=
+  par(nsepseq(entry_param_decl,SEMI))
+
+proc_decl ::=
+  Procedure Ident parameters Is
+    seq(local_decl)
+    block
+
+parameters ::=
+  par(nsepseq(param_decl,SEMI))
+
+param_decl ::=
+  Var   Ident COLON param_type
+| Const Ident COLON param_type
+
+entry_param_decl ::=
+  param_decl
+| Storage Ident COLON param_type
+
+param_type ::=
+  cartesian
+
+block ::=
+  Begin series(statement,SEMI,End)
+| Block LBRACE series(statement,SEMI,RBRACE)
+
+statement ::=
+  instruction
+| data_decl
+
+data_decl ::=
+  const_decl
+| var_decl
+
+const_decl ::=
+  Const unqualified_decl(EQUAL)
+
+var_decl ::=
+  Var unqualified_decl(ASS)
+
+local_decl ::=
+  fun_decl  option(SEMI)
+| proc_decl option(SEMI)
+| data_decl option(SEMI)
+
+unqualified_decl(op) ::=
+  Ident (* var *) COLON type_expr op expr
+
+instruction ::=
+  block
+| If expr Then if_clause option(SEMI) Else if_clause
+| case(instruction)
+| Ident instruction_1
+| loop
+| Fail expr
+| Skip
+| Patch path With structure
+| Remove expr From remove_suffix
+
+remove_suffix ::=
+  Map path
+| Set path
+
+instruction_1 ::=
+  arguments
+| ASS expr
+| brackets(expr) ASS expr
+| selections option(brackets(expr)) ASS expr
+
+path ::=
+  Ident option(selections)
+
+selections ::=
+  DOT nsepseq(selection,DOT)
+
+injection(Kind,element) ::=
+  Kind inj_sufffix(element)
+
+inj_suffix(element) ::=
+  series(element,SEMI,End)
+| End
+| LBRACKET bracketed(element)
+
+bracketed(element) ::=
+  series(element,SEMI,RBRACKET)
+| RBRACKET
+
+binding ::=
+  expr ARROW expr
+
+if_clause ::=
+  instruction
+| LBRACE series(statement,COMMA,RBRACE)
+
+case(rhs) ::=
+  Case expr Of case_suffix(rhs)
+
+case_suffix(rhs) ::=
+  cases(rhs) End
+| LBRACKET cases(rhs) RBRACKET
+
+cases(rhs) ::=
+  nsepseq(case_clause(rhs),VBAR)
+| VBAR nsepseq(case_clause(rhs),VBAR)
+
+case_clause(rhs) ::=
+  pattern ARROW rhs
+
+loop ::=
+  While expr block
+| For Ident for_suffix
+
+for_suffix ::=
+  ASS expr option(Down) To expr option(step_clause) block
+| In expr block
+| ARROW Ident In expr block
+
+step_clause ::=
+  Step expr
+
+(* Expressions *)
+
+interactive_expr ::=
+  expr EOF
+
+expr ::=
+  case(expr)
+| disj_expr
+
+disj_expr ::=
+  left_assoc(conj_expr,Or)
+
+conj_expr ::=
+  left_assoc(set_membership,And)
+
+set_membership ::=
+  core_expr Contains set_membership
+| comp_expr
+
+comp_expr ::=
+  left_assoc(cat_expr,op_comp)
+
+op_comp ::=
+  LT | LEQ | GT | GEQ | EQUAL | NEQ
+
+cat_expr ::=
+  right_assoc(cons_expr,CAT)
+
+cons_expr ::=
+  left_assoc(add_expr,CONS)
+
+add_expr ::=
+  left_assoc(mult_expr,add_op)
+
+add_op ::=
+  PLUS | MINUS
+
+mult_expr ::=
+  left_assoc(unary_expr,mult_op)
+
+mult_op ::=
+  TIMES | SLASH | Mod
+
+unary_expr ::=
+  MINUS core_expr
+| Not core_expr
+| core_expr
+
+core_expr ::=
+  Int
+| Nat
+| Mtz
+| Ident option(core_suffix)
+| String
+| Bytes
+| C_False
+| C_True
+| C_Unit
+| C_None
+| C_Some arguments
+| Constr option(arguments)
+| par(paren_expr)
+| injection(List,expr)
+| Nil
+| structure
+
+core_suffix ::=
+  brackets(expr) (* lookup *)
+| DOT nsepseq(selection,DOT) option(brackets(expr))
+| arguments
+
+paren_expr ::=
+  disj_expr option(paren_expr_1)
+| case(expr) option(paren_expr_2)
+
+paren_expr_1 ::=
+  COLON type_expr
+| COMMA nsepseq(expr,COMMA)
+
+paren_expr_2 ::=
+  COMMA nsepseq(expr,COMMA)
+
+structure ::=
+  injection(Map,binding)
+| injection(Set,expr)
+| record_expr
+
+selection ::=
+  Ident (* field_name *)
+| Int
+
+record_expr ::=
+  Record record_expr_suffix
+
+record_expr_suffix ::=
+  series(field_assignment,SEMI,End)
+| LBRACKET series(field_assignment,SEMI,RBRACKET)
+
+field_assignment ::=
+  Ident (* field_name *) EQUAL expr
+
+arguments ::=
+  par(nsepseq(expr,COMMA))
+
+(* Patterns *)
+
+pattern ::=
+  nsepseq(core_pattern,CONS)
+
+core_pattern ::=
+  Ident (* var *)
+| WILD
+| Int
+| String
+| C_Unit
+| C_False
+| C_True
+| C_None
+| C_Some par(core_pattern)
+| Constr option(tuple_pattern)
+| injection(List,core_pattern)
+| Nil
+| par(option(paren_pattern))
+
+paren_pattern ::=
+  core_pattern paren_pattern_suffix
+
+paren_pattern_suffix ::=
+  CONS pattern
+| COMMA nsepseq(core_pattern,COMMA)
+
+tuple_pattern ::=
+  par(nsepseq(core_pattern,COMMA))
diff --git a/src/parser/pascaligo/Doc/pascaligo_22.bnf b/src/parser/pascaligo/Doc/pascaligo_22.bnf
new file mode 100644
index 000000000..6eb0e8dc1
--- /dev/null
+++ b/src/parser/pascaligo/Doc/pascaligo_22.bnf
@@ -0,0 +1,433 @@
+right_assoc(item,op) ::=
+  item
+| item op right_assoc(item,op)
+
+left_assoc(item,op) ::=
+  right_assoc(item,op)
+
+option(item) :=
+  (**)
+| item
+
+series(item,sep,term) ::=
+  item after_item(item,sep,term)
+
+after_item(item,sep,term) ::=
+  sep item_or_closing(item,sep,term)
+| term
+
+item_or_closing(item,sep,term) ::=
+  term
+| series(item,sep,term)
+
+(* Compound constructs *)
+
+par(item) ::=
+  LPAR item RPAR
+
+brackets(item) ::=
+  LBRACKET item RBRACKET
+
+(* Sequences *)
+
+(* Possibly empty sequence of items
+
+   LL(1) constraint: item not in Follow(seq), where
+   Follow(seq) = Follow(nseq) = {EOF, Begin, Block}
+*)
+
+seq(item) ::=
+  option(nseq(item))
+
+(* Non-empty sequence of items *)
+
+nseq(item) ::=
+  item seq(item)
+
+(* Non-empty separated sequence of items *)
+
+nsepseq(item,Sep) ::=
+  item
+| item Sep nsepseq(item,Sep)
+
+(* Main *)
+
+contract ::=
+  nseq(declaration) EOF
+
+(* LL(1) constraint: SEMI not in Follow(declaration), where
+   Follow(declaration)
+      = {EOF} U First(declaration)
+      = {EOF} U First(type_decl)
+        U First(const_decl) U First(lambda_decl)
+      = {EOF} U {Type} U {Const} U First(fun_decl)
+        U First(proc_decl) U First(entry_decl)
+      = {EOF,Type,Const,Function,Procedure,Entrypoint}.
+*)
+
+declaration ::=
+  type_decl   option(SEMI)
+| const_decl  option(SEMI)
+| lambda_decl option(SEMI)
+
+(* Type declarations *)
+
+type_decl ::=
+  Type Ident Is type_expr
+
+type_expr ::=
+  cartesian
+| nsepseq(variant,VBAR)
+| VBAR nsepseq(variant,VBAR)
+| Record record_type_expr
+
+record_type_expr ::=
+  series(field_decl,SEMI,End)
+| LBRACKET series(field_decl,SEMI,RBRACKET)
+
+(* LL(1) constraint: Of not in Follow(variant).
+   "Of" only occurs after {Constr, expr}. *)
+
+variant ::=
+  Constr option(of_cartesian)
+
+of_cartesian ::=
+  Of cartesian
+
+cartesian ::=
+  nsepseq(function_type,TIMES)
+
+function_type ::=
+  right_assoc(core_type,ARROW)
+
+(* LL(1) constraint: LPAR not in Follow(core_type), where
+   Follow(core_type)
+     = {ARROW} U Follow(function_type)
+     = {ARROW} U {TIMES} U Follow(cartesian)
+     = {ARROW,TIMES} U Follow(of_cartesian) U Follow(type_expr)
+       U Follow(param_type)
+     = {ARROW,TIMES} U Follow(variant)
+       U {RPAR,COMMA,Is,EQUAL,ASS} U Follow(field_decl)
+       U Follow(paren_expr_1) U Follow(type_decl)
+       U Follow(param_decl) U Follow(entry_param_decl)
+     = {ARROW,TIMES,RPAR,COMMA,Is,EQUAL,ASS,VBAR,
+        SEMI,End,RBRACKET} U Follow(paren_expr)
+        U {SEMI} U Follow(declaration)
+     = {ARROW,TIMES,RPAR,COMMA,Is,EQUAL,ASS,VBAR,
+        SEMI,End,RBRACKET,EOF,Type,Const,
+        Function,Procedure,Entrypoint}.
+*)
+
+core_type ::=
+  Ident (* type_name *) option(type_tuple)
+| Map type_tuple
+| Set par(type_expr)
+| List par(type_expr)
+| par(type_expr)
+
+type_tuple ::=
+  par(nsepseq(type_expr,COMMA))
+
+field_decl ::=
+  Ident (* field_name *) COLON type_expr
+
+(* Function and procedure declarations *)
+
+lambda_decl ::=
+  fun_decl
+| proc_decl
+| entry_decl
+
+fun_decl ::=
+  Function Ident parameters COLON type_expr Is
+    seq(local_decl)
+    block
+  With expr
+
+entry_decl ::=
+  Entrypoint Ident entry_params COLON type_expr Is
+    seq(local_decl)
+    block
+  With expr
+
+entry_params ::=
+  par(nsepseq(entry_param_decl,SEMI))
+
+proc_decl ::=
+  Procedure Ident parameters Is
+    seq(local_decl)
+    block
+
+parameters ::=
+  par(nsepseq(param_decl,SEMI))
+
+param_decl ::=
+  Var   Ident COLON param_type
+| Const Ident COLON param_type
+
+entry_param_decl ::=
+  param_decl
+| Storage Ident COLON param_type
+
+param_type ::=
+  cartesian
+
+block ::=
+  Begin series(statement,SEMI,End)
+| Block LBRACE series(statement,SEMI,RBRACE)
+
+statement ::=
+  instruction
+| data_decl
+
+data_decl ::=
+  const_decl
+| var_decl
+
+const_decl ::=
+  Const unqualified_decl(EQUAL)
+
+var_decl ::=
+  Var unqualified_decl(ASS)
+
+(* LL(1) constraint: SEMI not in Follow(local_decl), where
+   Follow(local_decl)
+     = First(local_decl) U First(block)
+     = First(fun_decl) U First(proc_decl) U First(data_decl)
+       U {BEGIN,Block}
+     = {Function,Procedure,BEGIN,Block} U First(const_decl)
+       U First(var_decl)
+     = {Function,Procedure,BEGIN,Block,Const,Var}.
+*)
+
+local_decl ::=
+  fun_decl  option(SEMI)
+| proc_decl option(SEMI)
+| data_decl option(SEMI)
+
+unqualified_decl(op) ::=
+  Ident (* var *) COLON type_expr op expr
+
+instruction ::=
+  block
+| If expr Then if_clause option(SEMI) Else if_clause
+| case(instruction)
+| Ident instruction_1
+| loop
+| Fail expr
+| Skip
+| Patch path With structure
+| Remove expr From remove_suffix
+
+remove_suffix ::=
+  Map path
+| Set path
+
+instruction_1 ::=
+  arguments
+| ASS expr
+| brackets(expr) ASS expr
+| selections option(brackets(expr)) ASS expr
+
+(* LL(1) constraint: First(selections) not in Follow(path), where
+   First(selections) = {DOT} and
+   Follow(path)
+     = {With} U Follow(remove_suffix)
+     = {With} U Follow(instruction)
+     = {With} U Follow(statement) U Follow(if_clause)
+       U Follow(case_clause(instruction))
+     = {With,SEMI,End,Else,VBAR} U Follow(cases(instruction))
+     = {With,SEMI,End,Else,VBAR,RBRACKET}.
+*)
+
+path ::=
+  Ident option(selections)
+
+selections ::=
+  DOT nsepseq(selection,DOT)
+
+injection(Kind,element) ::=
+  Kind inj_sufffix(element)
+
+inj_suffix(element) ::=
+  series(element,SEMI,End)
+| End
+| LBRACKET bracketed(element)
+
+bracketed(element) ::=
+  series(element,SEMI,RBRACKET)
+| RBRACKET
+
+binding ::=
+  expr ARROW expr
+
+if_clause ::=
+  instruction
+| LBRACE series(statement,COMMA,RBRACE)
+
+case(rhs) ::=
+  Case expr Of case_suffix(rhs)
+
+case_suffix(rhs) ::=
+  cases(rhs) End
+| LBRACKET cases(rhs) RBRACKET
+
+cases(rhs) ::=
+  nsepseq(case_clause(rhs),VBAR)
+| VBAR nsepseq(case_clause(rhs),VBAR)
+
+case_clause(rhs) ::=
+  pattern ARROW rhs
+
+loop ::=
+  While expr block
+| For Ident for_suffix
+
+for_suffix ::=
+  ASS expr option(Down) To expr option(step_clause) block
+| In expr block
+| ARROW Ident In expr block
+
+step_clause ::=
+  Step expr
+
+(* Expressions *)
+
+interactive_expr ::=
+  expr EOF
+
+expr ::=
+  case(expr)
+| disj_expr
+
+disj_expr ::=
+  left_assoc(conj_expr,Or)
+
+conj_expr ::=
+  left_assoc(set_membership,And)
+
+set_membership ::=
+  comp_expr option(contains_clause)  (* Enlarged the language *)
+
+contains_clause ::=
+  Contains set_membership
+
+comp_expr ::=
+  left_assoc(cat_expr,op_comp)
+
+op_comp ::=
+  LT | LEQ | GT | GEQ | EQUAL | NEQ
+
+cat_expr ::=
+  right_assoc(cons_expr,CAT)
+
+cons_expr ::=
+  left_assoc(add_expr,CONS)
+
+add_expr ::=
+  left_assoc(mult_expr,add_op)
+
+add_op ::=
+  PLUS | MINUS
+
+mult_expr ::=
+  left_assoc(unary_expr,mult_op)
+
+mult_op ::=
+  TIMES | SLASH | Mod
+
+unary_expr ::=
+  MINUS core_expr
+| Not core_expr
+| core_expr
+
+(* LL(1) constraint: First(core_suffix) not in Follow(core_expr)
+   First(core_suffix) =
+
+XXX
+*)
+core_expr ::=
+  Int
+| Nat
+| Mtz
+| Ident option(core_suffix)
+| String
+| Bytes
+| C_False
+| C_True
+| C_Unit
+| C_None
+| C_Some arguments
+| Constr option(arguments)
+| par(paren_expr)
+| injection(List,expr)
+| Nil
+| structure
+
+core_suffix ::=
+  brackets(expr) (* lookup *)
+| DOT nsepseq(selection,DOT) option(brackets(expr))
+| arguments
+
+paren_expr ::=
+  disj_expr option(paren_expr_1)
+| case(expr) option(paren_expr_2)
+
+paren_expr_1 ::=
+  COLON type_expr
+| COMMA nsepseq(expr,COMMA)
+
+paren_expr_2 ::=
+  COMMA nsepseq(expr,COMMA)
+
+structure ::=
+  injection(Map,binding)
+| injection(Set,expr)
+| record_expr
+
+selection ::=
+  Ident (* field_name *)
+| Int
+
+record_expr ::=
+  Record record_expr_suffix
+
+record_expr_suffix ::=
+  series(field_assignment,SEMI,End)
+| LBRACKET series(field_assignment,SEMI,RBRACKET)
+
+field_assignment ::=
+  Ident (* field_name *) EQUAL expr
+
+arguments ::=
+  par(nsepseq(expr,COMMA))
+
+(* Patterns *)
+
+pattern ::=
+  nsepseq(core_pattern,CONS)
+
+core_pattern ::=
+  Ident (* var *)
+| WILD
+| Int
+| String
+| C_Unit
+| C_False
+| C_True
+| C_None
+| C_Some par(core_pattern)
+| Constr option(tuple_pattern)
+| injection(List,core_pattern)
+| Nil
+| par(option(paren_pattern))
+
+paren_pattern ::=
+  core_pattern paren_pattern_suffix
+
+paren_pattern_suffix ::=
+  CONS pattern
+| COMMA nsepseq(core_pattern,COMMA)
+
+tuple_pattern ::=
+  par(nsepseq(core_pattern,COMMA))