diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b9b6da3ed..366da11c4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -12,37 +12,32 @@ before_script:
   - chmod +x /usr/local/bin/opam
   - export PATH="/usr/local/bin${PATH:+:}${PATH:-}"
 
-  # Show environment
-  - echo "$PATH"
+  # Initialise opam
   - printf '' | opam init --bare
   - eval $(opam config env)
 
   # Create switch
   - printf '' | opam switch create toto ocaml-base-compiler.4.06.1
   - eval $(opam config env)
+
   # Show versions and current switch
+  - echo "$PATH"
   - opam --version
   - printf '' | ocaml
   - opam switch
 
-# default-job:
-#   script:
-#     - (cd src/lib_utils && opam install -y --build-test --working-dir .)
-#     - (cd src/ligo      && opam install -y --build-test --working-dir .)
-#     - (cd src/ligo      && dune build && dune build -p ligo && dune build @ligo-test)
-#   artifacts:
-#     paths:
-#       - src/ligo/bin/cli.ml
-
 local-dune-job:
   script:
     - vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
     - opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository-local/"
     - opam install -y --build-test --deps-only ./src/
-    - (dune build -p ligo)
+    - dune build -p ligo
     # TODO: also try instead from time to time:
     #- (cd ./src/; dune build -p ligo)
     - dune build @ligo-test
+#   artifacts:
+#     paths:
+#       - src/ligo/bin/cli.ml
 
 local-repo-job:
   script:
diff --git a/.gitmodules b/.gitmodules
index 638bce839..a225f004f 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +1,12 @@
 [submodule "vendors/ligo-opam-repository"]
 	path = vendors/ligo-opam-repository
 	url = https://gitlab.com/gabriel.alfour/ligo-opam-repository.git
+  pushurl = git@gitlab.com:gabriel.alfour/ligo-opam-repository.git
 [submodule "vendors/ligo-utils"]
 	path = vendors/ligo-utils
 	url = https://gitlab.com/gabriel.alfour/ligo-utils.git
+  pushurl = git@gitlab.com:gabriel.alfour/ligo-utils.git
 [submodule "vendors/tezos-modded"]
 	path = vendors/tezos-modded
 	url = https://gitlab.com/gabriel.alfour/tezos-modded.git
+  pushurl = git@gitlab.com:gabriel.alfour/tezos-modded.git
diff --git a/src/ast_simplified/PP.ml b/src/ast_simplified/PP.ml
index 6eed2f798..cd7f81d61 100644
--- a/src/ast_simplified/PP.ml
+++ b/src/ast_simplified/PP.ml
@@ -44,7 +44,7 @@ let rec expression ppf (e:expression) = match e with
   | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
   | E_lambda {binder;input_type;output_type;result;body} ->
       fprintf ppf "lambda (%s:%a) : %a {@;  @[<v>%a@]@;} return %a"
-        binder type_expression input_type type_expression output_type
+        binder type_annotation input_type type_annotation output_type
         block body annotated_expression result
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
diff --git a/src/ast_simplified/combinators.ml b/src/ast_simplified/combinators.ml
index 6744722a6..c17b457c9 100644
--- a/src/ast_simplified/combinators.ml
+++ b/src/ast_simplified/combinators.ml
@@ -137,8 +137,8 @@ let e_lambda (binder : string)
   : expression =
   E_lambda {
     binder = (make_name binder) ;
-    input_type = input_type ;
-    output_type = output_type ;
+    input_type = Some input_type ;
+    output_type = Some output_type ;
     result = (make_e_a result) ;
     body ;
   }
diff --git a/src/ast_simplified/types.ml b/src/ast_simplified/types.ml
index 583a13100..e09d12e59 100644
--- a/src/ast_simplified/types.ml
+++ b/src/ast_simplified/types.ml
@@ -47,8 +47,8 @@ and type_expression =
 
 and lambda = {
   binder: name ;
-  input_type: type_expression ;
-  output_type: type_expression ;
+  input_type: type_expression option;
+  output_type: type_expression option;
   result: ae ;
   body: block ;
 }
diff --git a/src/parser/pascaligo/.links b/src/parser/pascaligo/.links
index 34a1424ad..8af33d655 100644
--- a/src/parser/pascaligo/.links
+++ b/src/parser/pascaligo/.links
@@ -1,7 +1,7 @@
 $HOME/git/OCaml-build/Makefile
 $HOME/git/OCaml-build/Makefile.cfg
-$HOME/git/tezos/src/lib_utils/pos.mli
-$HOME/git/tezos/src/lib_utils/pos.ml
-$HOME/git/tezos/src/lib_utils/region.mli
-$HOME/git/tezos/src/lib_utils/region.ml
-Stubs/Tezos_utils.ml
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/pos.mli
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/pos.ml
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/region.mli
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/region.ml
+Stubs/Simple_utils.ml
diff --git a/src/parser/pascaligo/AST.ml b/src/parser/pascaligo/AST.ml
index d24c4b766..84930a580 100644
--- a/src/parser/pascaligo/AST.ml
+++ b/src/parser/pascaligo/AST.ml
@@ -199,10 +199,9 @@ and type_expr =
 
 and cartesian = (type_expr, times) nsepseq reg
 
-and variant = {  (* TODO: Constant constructors *)
-  constr  : constr;
-  kwd_of  : kwd_of;
-  product : cartesian
+and variant = {
+  constr : constr;
+  args   : (kwd_of * cartesian) option
 }
 
 and record_type = field_decl reg injection reg
diff --git a/src/parser/pascaligo/AST.mli b/src/parser/pascaligo/AST.mli
index 5a8df626e..7de078bea 100644
--- a/src/parser/pascaligo/AST.mli
+++ b/src/parser/pascaligo/AST.mli
@@ -184,9 +184,8 @@ and type_expr =
 and cartesian = (type_expr, times) nsepseq reg
 
 and variant = {
-  constr  : constr;
-  kwd_of  : kwd_of;
-  product : cartesian
+  constr : constr;
+  args   : (kwd_of * cartesian) option
 }
 
 and record_type = field_decl reg injection reg
diff --git a/src/parser/pascaligo/Doc/pascaligo.txt b/src/parser/pascaligo/Doc/pascaligo.txt
new file mode 100644
index 000000000..5b6b78696
--- /dev/null
+++ b/src/parser/pascaligo/Doc/pascaligo.txt
@@ -0,0 +1,393 @@
+INTERNAL DOCUMENTATION OF THE PARSER OF PASCALIGO (Pascal-like LIGO)
+
+This document describes the source code in the directory
+ligo/src/parser/pascaligo and some maintenance workflows.
+
+The directory contains the following:
+
+  Doc
+    The directory containing this documentation.
+
+  Tests
+    The directory containing tests.
+
+  Version.ml
+    A source containing a commit hash. It should be deleted, as Dune
+    knows how to generate and updated version.
+
+  dune
+    The Dune file for building the Pascaligo parser.
+
+  pascaligo.ml
+    A source needed for building the parser with Dune.
+
+  check_dot_git_is_dir.sh
+     A shell initially made to distinguish a git worktree from the
+     working directory (currently broken).
+
+  Stubs
+    A directory containing Tezos_utils.ml, which is ignored by Dune,
+    but linked from the parent directory ligo/src/parser/pascaligo
+    when building with the Christian's Makefile for OCaml
+    projects. (See http://github.com/rinderknecht/OCaml-build) Ignore
+    them.
+
+  .LexerMain.tag
+  .Lexer.ml.tag
+  .ParserMain.tag
+  .Parser.mly.tag
+  .links
+     As ligo/src/parser/pascaligo/Stubs/Tezos_utils.ml, these files
+     are only used by Christian's build system. Ignore them.
+
+  LexerMain.ml
+  ParserMain.ml
+    Source for two entry points enabling Christian's build system to
+    build only a standalone lexer or a standalone parser. Do not
+    change, unless you change EvalOpt and use Christian's build system.
+
+  LexerLog.ml
+  LexerLog.mli
+    Source for instantiating a standalone lexer for LexerMain.ml and
+    ParserMain.ml. Ignore them.
+
+  ParserLog.mli
+  ParserLog.ml
+    Source for printing the AST. Used by ParserMain.ml, pascaligo.ml
+    and the translator from this AST to the one needed by the
+    type-checker (see directory ligo/src/simplify).
+
+  Utils.mli
+  Utils.ml
+    Some utility types and functions.
+
+  AST.mli
+  AST.ml
+    The abstract syntax tree of Pascaligo.
+
+  EvalOpt.mli
+  EvalOpt.ml
+    The module EvalOpt parses the command-line for options to the
+    parser. That action is performed as a side-effect when the module
+    is initialised at run-time: this is ugly and easy to fix. See
+    ligo/src/parser/ligodity/EvalOpt.ml{i} for the right way to do
+    it. Ignore them: the file actually calling directly the parser is
+    ligo/src/parser/parser.ml. Note that, as a consequence, no option
+    is currently passed to the parser when building Pascaligo with
+    Dune. This should be made available.
+
+  Markup.mli
+  Markup.ml
+    The definition of markup in Pascaligo source files, and some some
+    functions to print or convert it to strings. You are unlikely
+    going to modify those files, as markup is pretty much the same for
+    all LIGO flavours.
+
+  FQueue.mli
+  FQueue.ml
+    A naive implementation of purely functional queues. Replace by an
+    imperative implementation if worst-case performance of single
+    operations (queue/enqueue) is an issue.
+
+  Error.mli
+    The definition of the open type for errors: the lexer will add its
+    own errors, the downside being that matching on errors requires a
+    catch-all clause "| _ -> assert false" at the end. Note: the rest
+    of the compiler uses an error monad.
+
+  Lexer.mli
+  Lexer.mll
+    The Pascaligo lexer is generated from two ocamllex
+    specifications. Lexer.mll is the first-level lexer. It exports a
+    functor [Make] parameterised over a module [Token] defining the
+    tokens, and returning a module whose signature is [Lexer.S]. (See
+    Lexer.mli for a rationale.) If you write a new flavour of LIGO,
+    this lexer is likely to be reused as is. Note that a great deal of
+    the complexity of this lexer stems from its purpose to report
+    stylistic errors (hence keeping temporarily scanned markup) and
+    handling UTF-8 encoded comments. The first goal implies sometimes
+    reading more than one token, and an extra-buffer has to be managed
+    above the ocamllex one, so the parser is not confused about the
+    location (region) of the token it has just read.
+
+  LexToken.mli
+  LexToken.mll
+    The second-level lexer of Pascaligo, scanning the (lexical)
+    tokens, and used to instantiate the first-level lexer
+    (Lexer.mll). If you write a new flavour of LIGO, this lexer is
+    likely to be modified, also if you plan to add new lexemes (beware
+    that if you add a new token constructor to the type [LexToken.t],
+    you may have to change the signature [Lexer.S] so you an instantiate
+    the first-level lexer.
+
+  Parser.mly
+    The Menhir specification of the grammar of Pascaligo and the
+    semantic actions building the AST. The syntax is actually a mix of
+    two sub-flavours: one in which compound structures, like blocks,
+    records, lists etc., are opened by a keyword denoting the kind of
+    structure, like "block", "record", "list" etc., and are closed by
+    the key word "end", and one in which those structures are opened
+    by a keyword followed by a symbol, like "{", "[" etc. and closed
+    by a symbol, lik "}", "]" etc. For instance,
+       "record x : t; y : u end" versus "record {x : t; y : u}".
+    In the future, these two styles should be separated and, in the
+    meantime, it is advise to keep to one style per LIGO contract, for
+    readability's sake. A first maintenance task would be to separate
+    this file in two, so each parses only one style, and share the
+    common parts of the grammar.
+      However you change this file, the grammar must remain without LR
+    conflicts, without resorting %prec or %assoc annotations.
+
+
+PASCALIGO
+
+Generalities
+
+Pascaligo is an imperative language for writing smart contracts on the
+Tezos blockchain. As such, it is compiled to Michelson, the native
+language of the Tezos blockchain. Its design is inspired by Pascal,
+OCaml and Michelson.
+
+  An imperative language is a language in which the value bound to a
+variable can change over time, as opposed to a constant. That change,
+called _side-effect_, is often leveraged through loops, enabling data
+to be modified and accumulated repeatedly. For example, here is how
+the integer value associated to the variable "x" is incremented by an
+instruction, called _assignment_:
+
+x := x + 1;
+
+A loop computing the sum of all integers from 1 to 10 would be written
+as follows:
+
+y := 0;
+for x := 1 to 10
+  begin
+    y := y + x
+  end
+
+(Note that this is useless in practice, as a closed-form formula
+exists for that computation.)
+
+  In Pascaligo, expressions and instructions are
+distinguished. Expressions are evaluated and yield values, whilst
+instructions are evaluated but do not yield values. Instructions are
+meant to perform side-effects, like changing the value of a variable,
+whereas expressions are purely computational, like calculating a an
+arithmetic means. Instructions and expressions can be compounded, and
+instructions can evaluate expressions as a means to perform
+side-effects.
+
+  Pascaligo is strongly and statically typed, which means that the
+composition of data and functions is contrained so the compiler can
+check that no such composition can fail at run-time, e.g., because of
+a meaningless expression. Pascaligo requires that variables are
+declared together with their type and an initial value.
+
+Declarations of values come in two kinds: either constants or
+variables. The former are assigned only once at their declaration, and
+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;
+
+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;
+
+Similarly, function declarations have their parameters and return
+value annotated with their types. For instance,
+
+function sum (const n : nat; const m : nat) : nat is
+  begin
+  end with n + m;
+
+declarares the function "sum" that takes as argument two constant
+natural numbers and return their sum. The expression whose value is
+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;
+  begin
+    if n <= 0 then f := 1
+    else
+      for m := 1 to n
+        begin
+          f := f * m
+        end
+   end with f
+
+Like Pascal, Pascaligo offers procedures, as well as functions. The
+difference follows the divide between expressions and instructions:
+function calls are expressions, procedure calls are instructions.
+
+A special case of functions are entry points, which are functions that
+can be called when interacting with the contract after it has been
+originated on the chain. The only difference with function is that
+they are introduced by a keyword "entrypoint", instead of "function",
+and they (currently) must have a special parameter for the storage,
+and the return type must be a pair made of a new storage and a list of
+operations. For example,
+
+entrypoint contribute (storage store : store; ...)
+  : store * list (operation) is
+  var operations : list (operation) := nil
+  begin
+  ...
+  end with (store, operations)
+
+where "storage" is a keyword.
+
+  Pascaligo features predefined types, like integers, natural numbers,
+mutez, strings, maps, lists etc. and constructs to combine those into
+structured types. Amongst those constructs are the records, which
+group and map names (_fields_) to values of potentially different
+types. For instance,
+
+type point is
+  record
+    x : int;
+    y : int
+  end
+
+defines a record type "store" with three fields, each made of a name
+and a type. Values of record types are made by assigning a value to
+each field (in any order). Like so:
+
+const origin : point =
+  record
+    x = 0;
+    y = 0
+  end
+
+At this point it is perhaps useful to remark that there are actually
+two flavours of Pascaligo recognised by the same parser: they should
+be separated in the future, and, for now, it is best to not mix both
+styles. Those style differ in the manner compound constructs are
+delimited
+
+For example, the type "point" above could have been alternatively
+defined as follows:
+
+type point is
+  record [
+    x : int;
+    y : int
+  ]
+
+and the value as
+
+const origin : point = record [x = 0; y = 0];
+
+When updating the contents of a record, Pascaligo offers some
+syntactic support. Instead of writing all the assignments, most of
+which are left unchanged, there is the record patch, which corresponds
+to a functional update in OCaml. For example,
+
+var p : point := origin;
+
+patch p with record y = 10 end;
+
+will update only the field "y" of "p". Of course, this example is not
+impressive, but imagine that one has to update a small number of
+fields in a large record. An alternative syntax is
+
+patch p with record [y = 10];
+
+  Another way to combine types are disjunctive types, which are a
+generalisation of enumerated types found in OCaml. They can be
+interpreted as being a disjoint partition of value sets, each being
+disinguished by a unique tag, or _data constructor_. For example,
+
+type u = unit
+type t = A | B of u | C of int * string
+
+See OCaml.
+
+As in OCaml, their values can be matched against patterns:
+
+match v with
+  A -> "A"
+| B Unit -> "B"
+| C (_, s) -> s
+
+Of course, we also find type aliases, which simply rename a type. More
+importantly, Pascaligo has predefined types that cannot be defined by
+the contract programmer. Indeed, user-defined types are monomorphic
+and non-recursive, in other words, they are not parameterised and
+cannot be defined in terms of themselves. This limitation precludes
+defining lists of values, as a list is an inductive data type: a list
+is either empty or a pair made of an item (the first item) and another
+list (the remaining items). That is why Pascaligo features a native
+polymorphic list type, with the condition that all list values must
+instantiate the type of the items it contains. Another useful data
+abstraction, native to Pascaligo, is the map, which relates values of
+a given type to values of another given type. The last type predefined
+by Pascaligo is the set.
+
+Pascaligo is inspired by Pascal and OCaml. Semi-colons are separators,
+but they can be used as terminators as well.
+
+For example
+
+type store is
+  record
+    goal     : nat;
+    deadline : timestamp;
+    backers  : map (address, nat);
+    funded   : bool;
+  end
+
+can alternatively be written
+
+type store is
+  record
+    goal     : nat;
+    deadline : timestamp;
+    backers  : map (address, nat);
+    funded   : bool
+  end
+
+Only non-recursive types are user-definable in LIGO.
+
+A predefined recursive and polymorphic type is the list (or
+stack). The syntax is the same as in OCaml, with some extra syntax for
+convenience. For example, the empty list can be written in three
+different ways (only one is recommended by contract):
+
+list end
+list []
+nil
+
+A non-empty list starts with the keyword "list" and comes in two
+flavours (only one is recommended by contract):
+
+list 1; 2; 3 end
+list [1; 2; 3]
+
+To push (cons) and element in a list, the infix operator is "::", as
+in OCaml:
+
+1::2::l
+
+All user-definable values in Pascaligo are monomorphic and must be
+annotated with a their types, except in arithmetic or boolean
+expressions, or at their declaration (since their type is given in the
+left-hand side). In particular, empty lists need to be annotated, like
+so
+
+1 :: (nil : list (int))
+
+But
+
+var l : list (int) := list [];
+
+works, as the type is available.
diff --git a/src/parser/pascaligo/Parser.mly b/src/parser/pascaligo/Parser.mly
index fa1030981..940825a13 100644
--- a/src/parser/pascaligo/Parser.mly
+++ b/src/parser/pascaligo/Parser.mly
@@ -213,9 +213,11 @@ sum_type:
 variant:
   Constr Of cartesian {
     let region = cover $1.region $3.region
-    and value = {constr = $1; kwd_of = $2; product = $3}
-    in {region; value} }
-  (* TODO: Unary constructors *)
+    and value = {constr = $1; args = Some ($2, $3)}
+    in {region; value}
+  }
+| Constr {
+    {region=$1.region; value= {constr=$1; args=None}} }
 
 record_type:
   Record series(field_decl,End) {
@@ -367,7 +369,6 @@ param_type:
   cartesian { TProd $1 }
 
 block:
-(*  Begin sequence(statement,SEMI) End { failwith "TODO" } *)
   Begin series(statement,End) {
    let first, (others, terminator, closing) = $2 in
    let region = cover $1 closing
@@ -706,7 +707,7 @@ assignment:
     in {region; value}}
 
 rhs:
-  expr   {     Expr $1 }
+  expr  { Expr $1 }
 
 lhs:
   path       {    Path $1 }
@@ -768,7 +769,7 @@ interactive_expr:
 
 expr:
   case(expr) { ECase ($1 expr_to_region) }
-| annot_expr  { $1                        }
+| annot_expr { $1                        }
 
 annot_expr:
   LPAR disj_expr COLON type_expr RPAR {
diff --git a/src/parser/pascaligo/ParserLog.ml b/src/parser/pascaligo/ParserLog.ml
index 27da8e846..61dcc9f2f 100644
--- a/src/parser/pascaligo/ParserLog.ml
+++ b/src/parser/pascaligo/ParserLog.ml
@@ -98,10 +98,13 @@ and print_cartesian {value; _} =
   print_nsepseq "*" print_type_expr value
 
 and print_variant {value; _} =
-  let {constr; kwd_of; product} = value in
+  let {constr; args} = value in
   print_constr    constr;
-  print_token     kwd_of "of";
-  print_cartesian product
+  match args with
+    None -> ()
+  | Some (kwd_of, product) ->
+      print_token     kwd_of "of";
+      print_cartesian product
 
 and print_sum_type {value; _} =
   print_nsepseq "|" print_variant value
diff --git a/src/parser/pascaligo/Stubs/Tezos_utils.ml b/src/parser/pascaligo/Stubs/Simple_utils.ml
similarity index 100%
rename from src/parser/pascaligo/Stubs/Tezos_utils.ml
rename to src/parser/pascaligo/Stubs/Simple_utils.ml
diff --git a/src/parser/pascaligo/Tests/crowdfunding.ligo b/src/parser/pascaligo/Tests/crowdfunding.ligo
index fd8607a59..bbd42dad7 100644
--- a/src/parser/pascaligo/Tests/crowdfunding.ligo
+++ b/src/parser/pascaligo/Tests/crowdfunding.ligo
@@ -14,7 +14,7 @@ entrypoint contribute (storage store : store;
      //  const s : list (int) = list [1; 2; 3]
 //const t : set (int) = set []
   begin
-    if now > store.deadline then
+    if now (Unit) > store.deadline then
       fail "Deadline passed";
     else
       case store.backers[sender] of [
diff --git a/src/simplify/camligo.ml b/src/simplify/camligo.ml
index 2b15bfe89..bba10ebc1 100644
--- a/src/simplify/camligo.ml
+++ b/src/simplify/camligo.ml
@@ -456,16 +456,17 @@ let let_entry : _ -> _ result = fun l ->
     List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)]
   in
   let%bind (body' , result) = expression_last_instruction (unwrap e) in
+  let input_type' = input_nty.type_expression in
+  let output_type' = O.(t_pair (t_list t_operation , storage_ty)) in
   let lambda =
-    let output_type = O.(t_pair (t_list t_operation , storage_ty)) in
     O.{
       binder = input_nty.type_name ;
-      input_type = input_nty.type_expression ;
-      output_type ;
+      input_type = Some input_type';
+      output_type = Some output_type';
       result ;
       body = tpl_declarations @ body' ;
     } in
-  let type_annotation = Some (O.T_function (lambda.input_type , lambda.output_type)) in
+  let type_annotation = Some (O.T_function (input_type', output_type')) in
   ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = {expression = O.E_lambda lambda ; type_annotation}}
 
 let let_init_storage : _ -> _ result = fun l ->
diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml
index 87944d47e..f9e281677 100644
--- a/src/simplify/pascaligo.ml
+++ b/src/simplify/pascaligo.ml
@@ -58,8 +58,13 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
       ok @@ T_record m
   | TSum s ->
       let aux (v:Raw.variant Raw.reg) =
+        let args =
+          match v.value.args with
+            None -> []
+          | Some (_, product) ->
+              npsseq_to_list product.value in
         let%bind te = simpl_list_type_expression
-          @@ npseq_to_list v.value.product.value in
+          @@ args in
         ok (v.value.constr.value, te)
       in
       let%bind lst = bind_list
@@ -345,7 +350,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
        let%bind result = simpl_expression return in
        let%bind output_type = simpl_type_expression ret_type in
        let body = local_declarations @ instructions in
-       let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
+       let expression = E_lambda {binder ; input_type = Some input_type;
+                                  output_type = Some output_type; result ; body } in
        let type_annotation = Some (T_function (input_type, output_type)) in
        ok {name;annotated_expression = {expression;type_annotation}}
      )
@@ -384,7 +390,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
 
        let body = tpl_declarations @ local_declarations @ instructions in
        let%bind result = simpl_expression return in
-       let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
+       let expression = E_lambda {binder ; input_type = Some input_type;
+                                  output_type = Some output_type; result ; body } in
        let type_annotation = Some (T_function (input_type, output_type)) in
        ok {name = name.value;annotated_expression = {expression;type_annotation}}
      )
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 4aa5d8498..bac549897 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -246,6 +246,14 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
   let return ?(tv = tv) expr = ok @@ Combinators.Expression.make_tpl (expr, tv) in
   let f = translate_annotated_expression in
   match ae.expression with
+    (* Optimise immediate application as a let-in *)
+  | E_application ({expression = E_lambda {binder; input_type; output_type=_; body=[]; result}; _},
+                   rhs) ->
+    let%bind ty' = translate_type input_type in
+    let%bind rhs' = translate_annotated_expression env rhs in
+    let result_env = Environment.(add (binder, ty') env) in
+    let%bind result' = translate_annotated_expression result_env result in
+    return (E_let_in ((binder, ty'), rhs', result'))
   | E_failwith ae -> (
       let%bind ae' = translate_annotated_expression ae in
       return @@ E_constant ("FAILWITH" , [ae'])
diff --git a/vendors/tezos-modded b/vendors/tezos-modded
index 378e4a590..044f4dfa5 160000
--- a/vendors/tezos-modded
+++ b/vendors/tezos-modded
@@ -1 +1 @@
-Subproject commit 378e4a590407517482952984571fba2e52962900
+Subproject commit 044f4dfa5974e627eab9bc1e3578b199182670fc