diff --git a/lexer.mll b/lexer.mll
index 5339075..b836aa9 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -15,9 +15,6 @@ rule token = parse
   | [' ' '\t' '\n']      { token lexbuf }
   | '.'             { DOT }
   | ','             { COMMA }
-  | '+'             { PLUS }
-  | '*'             { TIMES }
-  | "True"          { TOP }
   | "False"         { BOT }
   | '('             { LPAREN }
   | ')'             { RPAREN }
@@ -37,7 +34,6 @@ rule token = parse
   | "Qed"           { QED }
   | "exact"         { EXACT }
   | "assumption"    { ASSUMPTION }
-  | "destruct"      { DESTRUCT }
   | "intros"        { INTROS }
   | "intro"         { INTRO }
   | "cut"           { CUT }
@@ -45,6 +41,7 @@ rule token = parse
   | "left"          { LEFT }
   | "right"         { RIGHT }
   | "split"         { SPLIT }
+  | "try"           { TRY }
 
   | var_id as s     { VARID(s) }
   | ty_id as s      { TYID(s) }
diff --git a/main.ml b/main.ml
index d57f53b..e5c7de6 100644
--- a/main.ml
+++ b/main.ml
@@ -5,7 +5,7 @@ open Types
 open Hlam
 
 type entry =
-  Simple of (unit -> cmd)
+  Simple of (unit -> instr)
   | Reduce of Lam.lam
   | AlphaEquiv of Lam.lam * Lam.lam
 
@@ -14,11 +14,11 @@ type interactive_state = (hlam * ty) option * proof
 let parse_lam t =
   match Parser.main Lexer.token t with
   | Lam l -> l
-  | Cmd _ -> failwith "entry must be a lam"
+  | Instr _ -> failwith "entry must be a lam"
 
 let parse_cmd t =
   match Parser.main Lexer.token t with
-  | Cmd c -> c
+  | Instr is -> is
   | Lam _ -> failwith "entry must be a cmd"
 
 let show_beta_reduction e =
@@ -60,7 +60,7 @@ let alpha_get_lam where_from =
   - g, gs : next goals
   - sq : previous states of the interactive loop
 *)
-let rec interactive (get_cmd : unit -> cmd) (sl : (interactive_state) list) : proof =
+let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list) : proof =
   let (cg, (g, gs)), sq = match sl with
     [] -> (None, (None, [])), []
     | s::sq -> s, sq
@@ -72,38 +72,40 @@ let rec interactive (get_cmd : unit -> cmd) (sl : (interactive_state) list) : pr
     in
 
     try
-      match get_cmd () with
-      Goal ty ->
-        let rh = Ref (ref Hole) in
-        [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_cmd
-      | Undo -> interactive get_cmd sq
-      | Qed -> begin match cg with
-        None ->
-          print_error "No current goal" "";
-          (cg, (g, gs))::sq |> interactive get_cmd
-        | Some (h, t) ->
-          let l = lam_of_hlam h
-          |> beta_reduce in
-          if Typing.typecheck [] l t then begin
-            print_string "Ok";
-            [None, (None, [])] |> interactive get_cmd
-          end else begin
-            print_error "Typing failed" "";
-            print_expr l;
-            print_newline ();
-            print_ty t;
-            (cg, (g, gs))::sq |> interactive get_cmd
-          end
+      match get_instr () with
+      Cmd c -> begin match c with
+          Goal ty ->
+            let rh = Ref (ref Hole) in
+            [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
+          | Undo -> interactive get_instr sq
+          | Qed -> begin match cg with
+            None ->
+              print_error "No current goal" "";
+              (cg, (g, gs))::sq |> interactive get_instr
+            | Some (h, t) ->
+              let l = lam_of_hlam h
+              |> beta_reduce in
+              if Typing.typecheck [] l t then begin
+                print_string "Ok";
+                [None, (None, [])] |> interactive get_instr
+              end else begin
+                print_error "Typing failed" "";
+                print_expr l;
+                print_newline ();
+                print_ty t;
+                (cg, (g, gs))::sq |> interactive get_instr
+              end
+            end
         end
       | Tact t ->
-        (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_cmd
+        (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_instr
     with
       Parser.Error ->
         print_error "Invalid input" "";
-        (cg, (g, gs))::sq |> interactive get_cmd
+        (cg, (g, gs))::sq |> interactive get_instr
       | TacticFailed arg ->
         print_error "Tactic failed" arg;
-        (cg, (g, gs))::sq |> interactive get_cmd
+        (cg, (g, gs))::sq |> interactive get_instr
       | End_of_file | Lexer.Eof ->
         print_string "Bye!\n";
         (g, gs)
@@ -176,8 +178,8 @@ let recupere_entree () =
 let run () =
   try
     match recupere_entree () with
-     Simple get_cmd ->
-      let _ = interactive get_cmd [None, (None, [])] in ()
+     Simple get_instr ->
+      let _ = interactive get_instr [None, (None, [])] in ()
     | Reduce l ->
       let _ = show_beta_reduction l in ()
     | AlphaEquiv (l1, l2) -> begin
diff --git a/parser.mly b/parser.mly
index bd59195..cc7e38c 100644
--- a/parser.mly
+++ b/parser.mly
@@ -8,8 +8,7 @@ open Parser_entry
 %token EOF
 
 %token DOT COMMA
-%token PLUS TIMES
-%token TOP BOT EXFALSO TILDE
+%token BOT EXFALSO TILDE
 %token LPAREN RPAREN
 %token FUN ARR COLON TARR
 %token AND OR
@@ -18,7 +17,7 @@ open Parser_entry
 
 %token GOAL UNDO QED
 %token EXACT ASSUMPTION INTRO INTROS CUT APPLY
-%token LEFT RIGHT SPLIT DESTRUCT
+%token LEFT RIGHT SPLIT TRY
 %token L R
 
 %right TARR
@@ -33,26 +32,29 @@ open Parser_entry
 %%
 main:
   | e=expression EOF { Lam e }
-  | ts=nonempty_list(tactic) EOF { Cmd ts }
+  | ts=nonempty_list(instr) EOF { Instr ts }
 
-tactic:
-  | c=command DOT { c }
+instr:
+  | c=command DOT         { Cmd c }
+  | t=tactic DOT          { Tact t }
 
 command:
   | GOAL t=ty             { Goal t }
   | UNDO                  { Undo }
   | QED                   { Qed }
-  | EXACT e=expression    { Tact (Exact_term e) }
-  | EXACT s=TYID          { Tact (Exact_proof s) }
-  | ASSUMPTION            { Tact (Assumption) }
-  | INTROS                { Tact (Intros) }
-  | INTRO                 { Tact (Intro) }
-  | SPLIT                 { Tact (Split) }
-  | RIGHT                 { Tact (Right) }
-  | LEFT                  { Tact (Left) }
-  | CUT t=ty              { Tact (Cut t) }
-  | APPLY s=TYID          { Tact (Apply s) }
 
+tactic:
+  | EXACT e=expression    { TExact_term e }
+  | EXACT s=TYID          { TExact_proof s }
+  | ASSUMPTION            { TAssumption }
+  | INTROS                { TIntros }
+  | INTRO                 { TIntro }
+  | SPLIT                 { TSplit }
+  | RIGHT                 { TRight }
+  | LEFT                  { TLeft }
+  | CUT t=ty              { TCut t }
+  | APPLY s=TYID          { TApply s }
+  | TRY t=tactic          { TTry t }
 
 ty_annot:
   | id=VARID COLON t=ty     { (id, t) }
diff --git a/parser_entry.ml b/parser_entry.ml
index 407bd8c..a1578ec 100644
--- a/parser_entry.ml
+++ b/parser_entry.ml
@@ -3,11 +3,14 @@ open Types
 open Proof
 
 type cmd =
-  | Goal of ty
+  Goal of ty
   | Undo
   | Qed
+
+type instr =
+  Cmd of cmd
   | Tact of tactic
 
 type parser_entry =
   | Lam of lam
-  | Cmd of cmd list
+  | Instr of instr list
diff --git a/proof.ml b/proof.ml
index 5f7b63e..a949fd8 100644
--- a/proof.ml
+++ b/proof.ml
@@ -7,16 +7,17 @@ type goal = hlam * Types.ty * context
 type proof = goal option * goal list
 
 type tactic =
-  Exact_term of lam
-  | Exact_proof of id
-  | Assumption
-  | Intros
-  | Intro
-  | Cut of ty
-  | Apply of id
-  | Split
-  | Right
-  | Left
+  TExact_term of lam
+  | TExact_proof of id
+  | TAssumption
+  | TIntros
+  | TIntro
+  | TCut of ty
+  | TApply of id
+  | TSplit
+  | TRight
+  | TLeft
+  | TTry of tactic
 
 let hyp_count = ref 0
 let get_fresh_hyp () =
@@ -216,18 +217,19 @@ let tact_left ((g, gs) : proof) : proof =
       Some (new_h, t_l, cs), gs
     | _ -> raise (TacticFailed "Not a disjunction")
 
-let apply_tactic (p : proof) (t : tactic) : proof =
+let rec apply_tactic (p : proof) (t : tactic) : proof =
   match t with
-  Exact_term e -> tact_exact_term p e
-  | Exact_proof hyp -> tact_exact_proof p hyp
-  | Intros -> tact_intros p
-  | Intro -> tact_intro p
-  | Assumption -> tact_assumption p
-  | Cut t -> tact_cut p t
-  | Apply h -> tact_apply p h
-  | Split -> tact_split p
-  | Right -> tact_right p
-  | Left -> tact_left p
+  TExact_term e -> tact_exact_term p e
+  | TExact_proof hyp -> tact_exact_proof p hyp
+  | TIntros -> tact_intros p
+  | TIntro -> tact_intro p
+  | TAssumption -> tact_assumption p
+  | TCut t -> tact_cut p t
+  | TApply h -> tact_apply p h
+  | TSplit -> tact_split p
+  | TRight -> tact_right p
+  | TLeft -> tact_left p
+  | TTry t -> try apply_tactic p t with TacticFailed _ -> p
 
 
 let tact_try (p : proof) (t : tactic) : proof =