diff --git a/src/parser/ast_term.ml b/src/parser/ast_term.ml
index ce029f4a..bfb7a1c8 100644
--- a/src/parser/ast_term.ml
+++ b/src/parser/ast_term.ml
@@ -104,7 +104,7 @@ let rec pp_term out (e : term) : unit =
     let ppb out (x, t) = Fmt.fprintf out "@[<2>%s :=@ %a@]" x.name pp t in
     Fmt.fprintf out "@[@[<2>let@ %a@] in@ %a@]"
       (Util.pp_list ~sep:"and" ppb)
-      bs pp_sub bod
+      bs pp bod
   | Lambda (args, bod) ->
     Fmt.fprintf out "@[lam %a.@ %a@]" (Util.pp_list pp_tyvar) args pp_sub bod
   | Pi (args, bod) ->
diff --git a/src/parser/parse_term.ml b/src/parser/parse_term.ml
index 3bce1b90..5cc6b9cf 100644
--- a/src/parser/parse_term.ml
+++ b/src/parser/parse_term.ml
@@ -84,6 +84,10 @@ and p_term_atomic ?else_ ~f () =
   P.suspend @@ fun () ->
   P.try_or_l ?else_ ~msg:"expected atomic term" @@ p_term_atomic_cases ~f ()
 
+(* TODO: handle infix symbols, with a table (sym -> precedence * parser).
+   Start by registering "=" and "->" in there. *)
+(* TODO: handle lambda and pi *)
+
 (* parse application of [t] to 0 or more arguments *)
 and p_term_apply t args : A.term P.t =
   P.suspend @@ fun () ->
diff --git a/unittest/parser/p1.ml b/unittest/parser/p1.ml
index f42c7064..46fc9339 100644
--- a/unittest/parser/p1.ml
+++ b/unittest/parser/p1.ml
@@ -18,3 +18,10 @@ let test_str what s =
 
 let () = test_str "t1" "f (g x) y"
 let () = test_str "t2" "let x:= 1 in f (f x 2)"
+
+let () =
+  test_str "t3"
+    {|
+let l := map f (list 1 2 3) in
+let l2 := rev l in eq (rev l2) l
+    |}