diff --git a/src/ast_typed/combinators.ml b/src/ast_typed/combinators.ml
index 350836fc0..a6d34c72a 100644
--- a/src/ast_typed/combinators.ml
+++ b/src/ast_typed/combinators.ml
@@ -20,6 +20,7 @@ let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
 let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
 let t_nat ?s () : type_value = make_t (T_constant ("nat", [])) s
 let t_tez ?s () : type_value = make_t (T_constant ("tez", [])) s
+let t_timestamp ?s () : type_value = make_t (T_constant ("timestamp", [])) s
 let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
 let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
 let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
diff --git a/src/bin/cli.ml b/src/bin/cli.ml
index c65b45f3f..f7fb287f3 100644
--- a/src/bin/cli.ml
+++ b/src/bin/cli.ml
@@ -6,7 +6,9 @@ let error_pp out (e : error) =
   let message =
     let opt = e |> member "message" |> string in
     let msg = Option.unopt ~default:"" opt in
-    ": " ^ msg in
+    if msg = ""
+    then ""
+    else ": " ^ msg in
   let error_code =
     let error_code = e |> member "error_code" in
     match error_code with
@@ -20,7 +22,12 @@ let error_pp out (e : error) =
     match data with
     | `Null -> ""
     | _ -> " " ^ (J.to_string data) ^ "\n" in
-  Format.fprintf out "%s%s%s.\n%s" title error_code message data
+  let infos =
+    let infos = e |> member "infos" in
+    match infos with
+    | `Null -> ""
+    | _ -> " " ^ (J.to_string infos) ^ "\n" in
+  Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos
 
 
 let toplevel x =
@@ -71,7 +78,7 @@ let compile_file =
     let%bind contract =
       trace (simple_info "compiling contract to michelson") @@
       Ligo.Run.compile_contract_file source entry_point syntax in
-    Format.printf "Contract:\n%s\n" contract ;
+    Format.printf "%s\n" contract ;
     ok ()
   in
   let term =
@@ -86,7 +93,7 @@ let compile_parameter =
     let%bind value =
       trace (simple_error "compile-input") @@
       Ligo.Run.compile_contract_parameter source entry_point expression syntax in
-    Format.printf "Input:\n%s\n" value;
+    Format.printf "%s\n" value;
     ok ()
   in
   let term =
@@ -101,7 +108,7 @@ let compile_storage =
     let%bind value =
       trace (simple_error "compile-storage") @@
       Ligo.Run.compile_contract_storage source entry_point expression syntax in
-    Format.printf "Storage:\n%s\n" value;
+    Format.printf "%s\n" value;
     ok ()
   in
   let term =
diff --git a/src/compiler/compiler_type.ml b/src/compiler/compiler_type.ml
index 20daf075c..18ea463cf 100644
--- a/src/compiler/compiler_type.ml
+++ b/src/compiler/compiler_type.ml
@@ -22,6 +22,7 @@ module Ty = struct
     | Base_int -> return int_k
     | Base_string -> return string_k
     | Base_address -> return address_k
+    | Base_timestamp -> return timestamp_k
     | Base_bytes -> return bytes_k
     | Base_operation -> fail (not_comparable "operation")
 
@@ -48,6 +49,7 @@ module Ty = struct
     | Base_tez -> return tez
     | Base_string -> return string
     | Base_address -> return address
+    | Base_timestamp -> return timestamp
     | Base_bytes -> return bytes
     | Base_operation -> return operation
 
@@ -117,6 +119,7 @@ let base_type : type_base -> O.michelson result =
   | Base_tez -> ok @@ O.prim T_mutez
   | Base_string -> ok @@ O.prim T_string
   | Base_address -> ok @@ O.prim T_address
+  | Base_timestamp -> ok @@ O.prim T_timestamp
   | Base_bytes -> ok @@ O.prim T_bytes
   | Base_operation -> ok @@ O.prim T_operation
 
diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml
index 895b0754a..51867e490 100644
--- a/src/mini_c/PP.ml
+++ b/src/mini_c/PP.ml
@@ -16,6 +16,7 @@ let type_base ppf : type_base -> _ = function
   | Base_tez -> fprintf ppf "tez"
   | Base_string -> fprintf ppf "string"
   | Base_address -> fprintf ppf "address"
+  | Base_timestamp -> fprintf ppf "timestamp"
   | Base_bytes -> fprintf ppf "bytes"
   | Base_operation -> fprintf ppf "operation"
 
diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml
index ca445ee0e..6e5bb4906 100644
--- a/src/mini_c/types.ml
+++ b/src/mini_c/types.ml
@@ -4,6 +4,7 @@ type type_base =
   | Base_unit
   | Base_bool
   | Base_int | Base_nat | Base_tez
+  | Base_timestamp
   | Base_string | Base_bytes | Base_address
   | Base_operation
 
diff --git a/src/operators/operators.ml b/src/operators/operators.ml
index c7665ea9d..afb5d34af 100644
--- a/src/operators/operators.ml
+++ b/src/operators/operators.ml
@@ -42,6 +42,7 @@ module Simplify = struct
     ("bool" , "bool") ;
     ("operation" , "operation") ;
     ("address" , "address") ;
+    ("timestamp" , "timestamp") ;
     ("contract" , "contract") ;
     ("list" , "list") ;
     ("option" , "option") ;
@@ -60,8 +61,10 @@ module Simplify = struct
       ("int" , "INT") ;
       ("abs" , "ABS") ;
       ("amount" , "AMOUNT") ;
+      ("now" , "NOW") ;
       ("unit" , "UNIT") ;
       ("source" , "SOURCE") ;
+      ("sender" , "SENDER") ;
       ("failwith" , "FAILWITH") ;
     ]
 
@@ -169,14 +172,15 @@ module Typer = struct
     | Some t -> ok t
 
   let sub = typer_2 "SUB" @@ fun a b ->
-    let%bind () =
-      trace_strong (simple_error "Types a and b aren't numbers") @@
-      Assert.assert_true @@
-      List.exists (eq_2 (a , b)) [
-        t_int () ;
-        t_nat () ;
-      ] in
-    ok @@ t_int ()
+    if (eq_2 (a , b) (t_int ()))
+    then ok @@ t_int () else
+    if (eq_2 (a , b) (t_nat ()))
+    then ok @@ t_int () else
+    if (eq_2 (a , b) (t_timestamp ()))
+    then ok @@ t_int () else
+    if (eq_2 (a , b) (t_tez ()))
+    then ok @@ t_tez () else
+      fail (simple_error "Typing substraction, bad parameters.")
 
   let some = typer_1 "SOME" @@ fun a -> ok @@ t_option a ()
 
@@ -232,6 +236,8 @@ module Typer = struct
 
   let amount = constant "AMOUNT" @@ t_tez ()
 
+  let now = constant "NOW" @@ t_timestamp ()
+
   let transaction = typer_3 "CALL" @@ fun param amount contract ->
     let%bind () = assert_t_tez amount in
     let%bind contract_param = get_t_contract contract in
@@ -264,6 +270,8 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
+    if eq_1 a (t_tez ()) && eq_1 b (t_nat ())
+    then ok @@ t_tez () else
       simple_fail "Dividing with wrong types"
 
   let mod_ = typer_2 "MOD" @@ fun a b ->
@@ -276,9 +284,11 @@ module Typer = struct
     then ok @@ t_nat () else
     if eq_2 (a , b) (t_int ())
     then ok @@ t_int () else
+    if eq_2 (a , b) (t_tez ())
+    then ok @@ t_tez () else
     if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
     then ok @@ t_int () else
-      simple_fail "Adding with wrong types"
+      simple_fail "Adding with wrong types. Expected nat, int or tez."
 
   let constant_typers = Map.String.of_list [
       add ;
@@ -312,6 +322,7 @@ module Typer = struct
       transaction ;
       get_contract ;
       abs ;
+      now ;
     ]
 
 end
@@ -364,6 +375,7 @@ module Compiler = struct
     ("CONS" , simple_binary @@ prim I_CONS) ;
     ("UNIT" , simple_constant @@ prim I_UNIT) ;
     ("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
+    ("NOW" , simple_constant @@ prim I_NOW) ;
     ("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
     ("SOURCE" , simple_constant @@ prim I_SOURCE) ;
     ("SENDER" , simple_constant @@ prim I_SENDER) ;
diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml
index 6925d2ba5..58b5d6896 100644
--- a/src/simplify/pascaligo.ml
+++ b/src/simplify/pascaligo.ml
@@ -346,7 +346,7 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
 
 and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result =
   match lst with
-  | [] -> assert false
+  | [] -> ok @@ t_unit
   | [hd] -> simpl_type_expression hd
   | lst ->
       let%bind lst = bind_list @@ List.map simpl_type_expression lst in
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 4b27b2dcc..724a32b32 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -93,6 +93,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
   | T_constant ("tez", []) -> ok (T_base Base_tez)
   | T_constant ("string", []) -> ok (T_base Base_string)
   | T_constant ("address", []) -> ok (T_base Base_address)
+  | T_constant ("timestamp", []) -> ok (T_base Base_timestamp)
   | T_constant ("unit", []) -> ok (T_base Base_unit)
   | T_constant ("operation", []) -> ok (T_base Base_operation)
   | T_constant ("contract", [x]) ->
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index 99d49144d..a3f0f0140 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -206,6 +206,13 @@ module Errors = struct
     ] in
     error ~data title message ()
 
+  let constant_error loc =
+    let title () = "typing constant" in
+    let message () = "" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
+    ] in
+    error ~data title message
 end
 open Errors
 
@@ -377,14 +384,13 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
     ok @@ make_a_e ~location expr tv e in
   let main_error =
     let title () = "typing expression" in
-    let content () =
-      match L.get () with
-      | "" ->
-        Format.asprintf "Expression: %a\n" I.PP.expression ae
-      | l ->
-        Format.asprintf "Expression: %a\nLog: %s\n" I.PP.expression ae l
-    in
-    error title content in
+    let content () = "" in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("location" , fun () -> Format.asprintf "%a" Location.pp @@ Location.get_location ae) ;
+      ("misc" , fun () -> L.get ()) ;
+    ] in
+    error ~data title content in
   trace main_error @@
   match Location.unwrap ae with
   (* Basic *)
@@ -563,7 +569,8 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
   | E_constant (name, lst) ->
       let%bind lst' = bind_list @@ List.map (type_expression e) lst in
       let tv_lst = List.map get_type_annotation lst' in
-      let%bind (name', tv) = type_constant name tv_lst tv_opt ae.location in
+      let%bind (name', tv) =
+        type_constant name tv_lst tv_opt ae.location in
       return (E_constant (name' , lst')) tv
   | E_application (f, arg) ->
       let%bind f' = type_expression e f in
@@ -731,6 +738,7 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
   let%bind typer =
     trace_option (unrecognized_constant name loc) @@
     Map.String.find_opt name ct in
+  trace (constant_error loc) @@
   typer lst tv_opt
 
 let untype_type_value (t:O.type_value) : (I.type_expression) result =