diff --git a/main.ml b/main.ml
index b484eca..9eb1289 100644
--- a/main.ml
+++ b/main.ml
@@ -1,8 +1,14 @@
 open Structs;;
 open Pieuvre;;
-
-let fail () =
-    failwith "Unknown error";;
+open Tactic;;
+    
+(* Lorsqu'une tactique ne peut se lancer. Contient la tactique ainsi qu'un message contenant l'erreur.*)
+exception TacticException of tactic*string;;
+(* Lorsqu'une tactique est mal écrite*)
+exception TacticParseException;;
+(* Exception renvoyée lorsque la fonction de trou est appelée sur une liste trop grande. *)
+(* Ne devrait jamais être lancée *)
+exception TrouException;;
 
 (* Parsage des arguments*)
 let filename = ref "" in
@@ -154,112 +160,125 @@ while !subgoals <> [] do
         Printf.printf "What do you want to do?\n"
     );
 
-    let tactic =
-        let rec read_tactic () =
-            try
-                let lexbuf = Lexing.from_string (readline ()) in
-                Parser.main_tactic Lexer.token lexbuf
-            with e -> (
-                  Printf.printf "Can't parse tactic\n";
-                  if is_interactive then
-                      read_tactic ()
-                  else
-                      raise e
-            )
-        in
-        read_tactic ()
+    let rec read_tactic () =
+        try
+            let lexbuf = Lexing.from_string (readline ()) in
+            Parser.main_tactic Lexer.token lexbuf
+        with e -> raise TacticParseException
     in
+    
+    let applyTactic tactic =
+        begin
+        let f = !fill_holes in
+        match tactic with
+        | Intro var -> (
+                match ty with
+                | TImpl (ty1, ty2) -> (
+                        subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                        | h :: hs -> f (LFun (var, ty1, h) :: hs)
+                        | _ -> raise TrouException
+                    )
+                | _ -> raise (TacticException(tactic,"Cannot intro when the goal is no implication."))
+            )
+        | Assumption -> (
+                let rec explore = function
+                | (var, hyp) :: _ when hyp = ty -> (
+                        fill_holes := fun holes -> f ((LVar var) :: holes)
+                    )
+                | [] -> raise (TacticException(tactic,"Cannot find a tactic that equals the goal."))
+                | _ :: hyps -> explore hyps
+                in
+                explore hyps
+            )
+        | Apply var -> (
+                match find_hyp var with
+                | Some (TImpl (t1, t2)) when t2 = ty -> (
+                        subgoals := (t1, hyps) :: !subgoals;
+                        fill_holes := function
+                        | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
+                        | [] -> raise TrouException
+                    )
+                | None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist."))
+                | _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is no implication."))
+            )
+        | Elim var -> (
+                match find_hyp var with
+                | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
+                | Some TAnd(tl,tr) -> (
+                        subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals;
+                        fill_holes := fun holes -> match holes with
+                        | h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r)
+                        | _ -> raise TrouException
+                    )
+                | Some TOr(tl,tr) -> (
+                        subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals;
+                        fill_holes := fun holes -> match holes with
+                        | hl::hr::r -> f (LCase(LVar(var),hl,hr)::r)
+                        | _ -> raise TrouException
+                    )
+                | None -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it does not exist."))
+                | _ -> raise (TacticException(tactic,"Cannot apply hypotesis "^var^" as it is neither an implication, nor a /\\ or a \\/"))
+            )
+        (* Pour montrer A, on montre B -> A et B *)
+        | Cut tint -> (
+                subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
+                fill_holes := function
+                | pf :: px :: s -> f ((LApp (pf, px)) :: s)
+                | _ -> raise TrouException
+            )
 
-    let f = !fill_holes in
-
-    match tactic with
-      | Intro var -> (
-            match ty with
-              | TImpl (ty1, ty2) -> (
-                    subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | h :: hs -> f (LFun (var, ty1, h) :: hs)
-                      | _ -> fail ()
-                )
-              | _ -> failwith "Can't intro"
-        )
-      | Assumption -> (
-            let rec explore = function
-              | (var, hyp) :: _ when hyp = ty -> (
-                    fill_holes := fun holes -> f ((LVar var) :: holes)
-                )
-              | [] -> failwith "No such hypothesis"
-              | _ :: hyps -> explore hyps
-            in
-            explore hyps
-        )
-      | Apply var -> (
-            match find_hyp var with
-              | Some (TImpl (t1, t2)) when t2 = ty -> (
-                    subgoals := (t1, hyps) :: !subgoals;
-                    fill_holes := function
-                      | hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
-                      | [] -> fail ()
-                )
-              | None -> failwith ("Hypothesis " ^ var ^ " not found")
-              | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
-        )
-      | Elim var -> (
-            match find_hyp var with
-              | Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
-              | Some TAnd(tl,tr) -> (
-                    subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r)
-                      | _ -> fail ()
-                )
-              | Some TOr(tl,tr) -> (
-                    subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | hl::hr::r -> f (LCase(LVar(var),hl,hr)::r)
-                      | _ -> fail ()
-                )
-              | None -> failwith ("Hypothesis " ^ var ^ " not found")
-              | _ -> failwith ("Hypothesis " ^ var ^ " unusable")
-        )
-      (* Pour montrer A, on montre B -> A et B *)
-      | Cut tint -> (
-            subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
-            fill_holes := function
-              | pf :: px :: s -> f ((LApp (pf, px)) :: s)
-              | _ -> fail ()
-        )
-
-      | Split ovar -> (
-            match ty with
-              | TAnd(t1,t2) -> (
-                    subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
-                      | _ -> fail ()
-                )
-              | _ -> failwith "Target not a and clause"
-        )
-      | Left -> (
-            match ty with
-              | TOr(tl,tr) -> (
-                    subgoals := (tl, hyps) :: !subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | hl :: hs -> f (LIg(hl,tr) :: hs)
-                      | _ -> fail ()
-                )
-              | _ -> failwith "Target not a or clause"
-        )
-      | Right -> (
-            match ty with
-              | TOr(tl,tr) -> (
-                    subgoals := (tr, hyps) :: !subgoals;
-                    fill_holes := fun holes -> match holes with
-                      | hr :: hs -> f (LId(hr,tl) :: hs)
-                      | _ -> fail ()
-                )
-              | _ -> failwith "Target not a or clause"
-        )
+        | Split -> (
+                match ty with
+                | TAnd(t1,t2) -> (
+                        subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                        | h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
+                        | _ -> raise TrouException
+                    )
+                | _ -> raise (TacticException(tactic,"Cannot split as the goal is no /\\ clause"))
+            )
+        | Left -> (
+                match ty with
+                | TOr(tl,tr) -> (
+                        subgoals := (tl, hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                        | hl :: hs -> f (LIg(hl,tr) :: hs)
+                        | _ -> raise TrouException
+                    )
+                | _ -> raise (TacticException(tactic,"Cannot prove left as the goal is no \\/ clause"))
+            )
+        | Right -> (
+                match ty with
+                | TOr(tl,tr) -> (
+                        subgoals := (tr, hyps) :: !subgoals;
+                        fill_holes := fun holes -> match holes with
+                        | hr :: hs -> f (LId(hr,tl) :: hs)
+                        | _ -> raise TrouException
+                    )
+                | _ -> raise (TacticException(tactic,"Cannot prove right as the goal is no \\/ clause"))
+            )
+        end
+    in
+    
+    let rec applyUntilWorking () =
+        try
+            (
+                let readTactic = read_tactic () in
+                    applyTactic readTactic
+            )
+        with
+            | TacticException(t,s) -> 
+                Printf.printf "\027[31mCannot apply the tactic: %s\027[0m\n" s;
+                if(is_interactive) then applyUntilWorking () else raise (TacticException(t,s))
+            | TacticParseException -> 
+                Printf.printf "\027[31mCannot parse the tactic, please refer to pieuvre documentation.\027[0m\n";
+                if(is_interactive) then applyUntilWorking () else raise TacticParseException
+            | e -> 
+                Printf.printf "\027[31mPieuvre Failed Unexpectedly !\027[0m\n";
+                raise e
+    in
+    applyUntilWorking ()
 done;
 
 let finalLam = !fill_holes [] in
diff --git a/parser.mly b/parser.mly
index 84a7655..14ed0e3 100644
--- a/parser.mly
+++ b/parser.mly
@@ -70,8 +70,7 @@ tactic:
   | APPLY VAR_NAME DOT                    { Apply $2 }
   | ELIM VAR_NAME DOT                     { Elim $2 }
   | CUT ty DOT                            { Cut $2 }
-  | SPLIT DOT                             { Split None }
-  | SPLIT VAR_NAME DOT                    { Split (Some $2) }
+  | SPLIT DOT                             { Split }
   | LEFT DOT                              { Left }
   | RIGHT DOT                             { Right }
 
diff --git a/pieuvre.ml b/pieuvre.ml
index 8182c56..45d040a 100644
--- a/pieuvre.ml
+++ b/pieuvre.ml
@@ -174,8 +174,8 @@ let rec betastep (l: lam) : lam option = match l with
         | (LCouple(lg,ld),None) -> Some ld
         | (_,None) -> None
         end
-    | LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(ll,t)))
-    | LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(ll,t)))
+    | LIg(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LIg(l',t)))
+    | LId(ll,t) -> Option.bind (betastep ll) (fun l' -> Some (LId(l',t)))
     | LCase(ll,lg,ld) ->  begin
         match (ll,betastep ll) with
         | (_,Some ll') -> Some (LFst(ll'))
diff --git a/tactic.ml b/tactic.ml
index 33e4669..4afcb6f 100644
--- a/tactic.ml
+++ b/tactic.ml
@@ -6,6 +6,6 @@ type tactic =
   | Apply of var_lambda
   | Elim of var_lambda
   | Cut of ty
-  | Split of var_lambda option
+  | Split
   | Left
   | Right;;