diff --git a/lexer.mll b/lexer.mll
index d4bb46b..c68d9bf 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -27,7 +27,7 @@ rule token = parse
 
   | "fun"                       { FUN }
   | "=>"                        { MAPS_TO }
-  | ':'                         { VDOTS }
+  | ':'                         { COLON }
   | "exf"                       { EXF }
   | "fst"                       { FST }
   | "snd"                       { SND }
diff --git a/main.ml b/main.ml
index be53aa0..b484eca 100644
--- a/main.ml
+++ b/main.ml
@@ -77,28 +77,27 @@ if !alpha_option then (
     exit 0
 );
 
-(*if !typecheck_option then (
+if !typecheck_option then (
     let lexbuf = Lexing.from_channel (match file with
       | None -> stdin
       | Some file -> file
     )
     in
-    let lambda_term =
+    let lambda_term, ty =
         try
-            Parser.main_lambda Lexer.token lexbuf
+            Parser.main_typed_lambda Lexer.token lexbuf
         with e -> (
-            Printf.printf "Can't read lambda term\n";
+            Printf.printf "Can't read typed lambda term\n";
             raise e
        )
     in
     Printf.printf "The type of %s is " (string_of_lam lambda_term);
-    if typecheck [] lambda_term then (
-        Printf.printf "correct\n"
-    ) else (
-        Printf.printf "incorrect\n"
+    if not (typecheck [] lambda_term ty) then (
+        Printf.printf "not "
     );
+    Printf.printf "%s.\n" (string_of_ty ty);
     exit 0
-);*)
+);
 
 (* Show a message only if the input is read from stdin *)
 let show s = match file with
@@ -137,7 +136,6 @@ while !subgoals <> [] do
         explore hyps
     in
 
-
     if is_interactive then (
         (* Nettoyage du terminal *)
         let _ = Sys.command("clear -x") in
@@ -267,7 +265,7 @@ done;
 let finalLam = !fill_holes [] in
     if (typecheck [] finalLam ty) then (
         Printf.printf "Final proof :\n";
-        reduce finalLam
+        reduce finalLam;
     )
     else (
         Printf.printf "Invalid proof constructed!\n";
diff --git a/parser.mly b/parser.mly
index 27b3fb9..84a7655 100644
--- a/parser.mly
+++ b/parser.mly
@@ -11,7 +11,7 @@
 %token <string> TYPE_NAME
 
 %token DOT INTRO ASSUMPTION APPLY ELIM CUT SPLIT LEFT RIGHT FST SND IG ID CASE
-%token FUN MAPS_TO VDOTS EXF
+%token FUN MAPS_TO COLON EXF
 
 %token AMPERSAND
 
@@ -33,6 +33,9 @@
 %start main_two_lambda
 %type <Structs.lam * Structs.lam> main_two_lambda
 
+%start main_typed_lambda
+%type <Structs.lam * Structs.ty> main_typed_lambda
+
 %%
 main_type:
   | ty EOF                                { $1 }
@@ -44,7 +47,10 @@ main_lambda:
   | lambda EOF                            { $1 }
 
 main_two_lambda:
-  | lambda AMPERSAND lambda               { $1, $3 }
+  | lambda AMPERSAND lambda EOF           { $1, $3 }
+
+main_typed_lambda:
+  | lambda COLON ty EOF                   { $1, $3 }
 
 /* Types */
 ty:
@@ -68,7 +74,7 @@ tactic:
   | SPLIT VAR_NAME DOT                    { Split (Some $2) }
   | LEFT DOT                              { Left }
   | RIGHT DOT                             { Right }
-  
+
 /* Lambda-termes */
 lambda_arg: /* Expression pouvant être en argument d'une fonction */
   | VAR_NAME                              { LVar $1 }
@@ -81,7 +87,7 @@ lambda_app:
 
 lambda:
   | lambda_app                            { $1 }
-  | FUN VAR_NAME VDOTS ty MAPS_TO lambda  { LFun ($2, $4, $6) }
-  | FUN LPAREN VAR_NAME VDOTS ty RPAREN MAPS_TO lambda
+  | FUN VAR_NAME COLON ty MAPS_TO lambda  { LFun ($2, $4, $6) }
+  | FUN LPAREN VAR_NAME COLON ty RPAREN MAPS_TO lambda
                                           { LFun ($3, $5, $8) }
-  | EXF LPAREN VAR_NAME VDOTS ty RPAREN   { LExf (LVar $3, $5) }
+  | EXF LPAREN VAR_NAME COLON ty RPAREN   { LExf (LVar $3, $5) }
diff --git a/tests/typecheck/right-type b/tests/typecheck/right-type
new file mode 100644
index 0000000..b6eac10
--- /dev/null
+++ b/tests/typecheck/right-type
@@ -0,0 +1 @@
+fun x: A => fun f: A -> False => f x : A -> ~~A
diff --git a/tests/typecheck/wrong-type b/tests/typecheck/wrong-type
new file mode 100644
index 0000000..9036bbb
--- /dev/null
+++ b/tests/typecheck/wrong-type
@@ -0,0 +1 @@
+(fun x: A -> A => x x) : A -> A