diff --git a/main.ml b/main.ml
index cba0a59..a1ea649 100644
--- a/main.ml
+++ b/main.ml
@@ -60,7 +60,11 @@ let alpha_get_lam where_from =
   - g, gs : next goals
   - sq : previous states of the interactive loop
 *)
-let rec interactive ((cg, (g, gs))::sq : (interactive_state) list) : proof =
+let rec interactive (sl : (interactive_state) list) : proof =
+  let (cg, (g, gs)), sq = match sl with
+    [] -> (None, (None, [])), []
+    | s::sq -> s, sq
+  in
   begin
     let _ = match g with
     None -> print_string "\n\027[1mNo more goals.\027[0m\n"
@@ -85,6 +89,9 @@ let rec interactive ((cg, (g, gs))::sq : (interactive_state) list) : proof =
             interactive [None, (None, [])]
           end else begin
             print_error "Typing failed" "";
+            (* print_expr l;
+            print_newline ();
+            print_ty t; *)
             (cg, (g, gs))::sq |> interactive
           end
         end