diff --git a/main.ml b/main.ml
index a0ed807..be53aa0 100644
--- a/main.ml
+++ b/main.ml
@@ -77,7 +77,7 @@ 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
@@ -92,13 +92,13 @@ if !typecheck_option then (
        )
     in
     Printf.printf "The type of %s is " (string_of_lam lambda_term);
-    if typecheck lambda_term then (
+    if typecheck [] lambda_term then (
         Printf.printf "correct\n"
     ) else (
         Printf.printf "incorrect\n"
     );
     exit 0
-);
+);*)
 
 (* Show a message only if the input is read from stdin *)
 let show s = match file with
@@ -137,7 +137,7 @@ while !subgoals <> [] do
         explore hyps
     in
 
-    
+
     if is_interactive then (
         (* Nettoyage du terminal *)
         let _ = Sys.command("clear -x") in
@@ -231,7 +231,7 @@ while !subgoals <> [] do
               | pf :: px :: s -> f ((LApp (pf, px)) :: s)
               | _ -> fail ()
         )
-    
+
       | Split ovar -> (
             match ty with
               | TAnd(t1,t2) -> (