diff --git a/TODO b/TODO
index bd9aa91..b9e59a1 100644
--- a/TODO
+++ b/TODO
@@ -1,14 +1,11 @@
 (* calculus_misc should populate himself during the process *)
 0) pprinter / parser
-   + test1.p passed line by line in regression
-   - Enhanced
 1) calculus_substitution
-   - need to be tested
 2) reduction
-   - need to be tested
 3) unification
-   - add match
+   - need to add flushing of terms 
+   - higher order unification
 4) terminfer
    - add using conversion when not solvable
 5) termcheck
-   - add final implicit
+
diff --git a/src/core/kernel/calculus_def.ml b/src/core/kernel/calculus_def.ml
index 6dbac10..88beb00 100644
--- a/src/core/kernel/calculus_def.ml
+++ b/src/core/kernel/calculus_def.ml
@@ -81,6 +81,7 @@ and pattern = PAvar | PName of string
 
 and typeannotation = NoAnnotation
 		     | Annotation of term
+		     | TypedAnnotation of term
 		     | Typed of term
 
 
@@ -129,6 +130,7 @@ type poussin_error = FreeError of string
 		    | NegativeIndexBVar of int
 		    | UnknownBVar of context * int
 		    | UnknownFVar of context * int
+		    | NotInductiveDestruction of context * term
 
 
 exception PoussinException of poussin_error
diff --git a/src/core/kernel/calculus_misc.ml b/src/core/kernel/calculus_misc.ml
index f7314b4..b0c6441 100644
--- a/src/core/kernel/calculus_misc.ml
+++ b/src/core/kernel/calculus_misc.ml
@@ -32,6 +32,9 @@ let lambda_ ?(annot: typeannotation = NoAnnotation) ?(posq: position = NoPositio
 let forall_ ?(annot: typeannotation = NoAnnotation) ?(posq: position = NoPosition) ?(posl: position = NoPosition) (name: name) ?(nature: nature = Explicit) ?(ty: term = avar_ ()) (body: term) : term =
   Forall ((name, ty, nature, posl), body, annot, posl, false)
 
+let app_ ?(annot: typeannotation = NoAnnotation) ?(pos: position = NoPosition) f args =
+  App (f, args, annot, pos, false)
+
 (* function for deconstructing/constructing contiguous lambdas *)
 let rec destruct_lambda (te: term) : ((name * term * nature * position) * typeannotation * position) list * term =
   match te with
@@ -82,6 +85,29 @@ let set_term_annotation (te: term) (ty: term) : term =
     | Match (te, des, _, pos, reduced) ->
       Match (te, des, Annotation ty, pos, reduced)
 
+let set_term_tannotation (te: term) (ty: term) : term =
+  match te with
+    | Universe (ty, lvl, pos) -> 
+      Universe (ty, lvl, pos)
+    | Cste (n, _, pos, reduced) ->
+      Cste (n, TypedAnnotation ty, pos, reduced)
+    | Var (i, _, pos) ->
+      Var (i, TypedAnnotation ty, pos)
+    | AVar (_, pos) ->
+      AVar (TypedAnnotation ty, pos)
+    | TName (n, _, pos) ->
+      TName (n, TypedAnnotation ty, pos)
+    | Lambda (q, te, _, pos, reduced) ->
+      Lambda (q, te, TypedAnnotation ty, pos, reduced)
+    | Forall (q, te, _, pos, reduced) ->
+      Forall (q, te, TypedAnnotation ty, pos, reduced)
+    | Let (q, te, _, pos, reduced) ->
+      Let (q, te, TypedAnnotation ty, pos, reduced)
+    | App (f, args, _, pos, reduced) ->
+      App (f, args, TypedAnnotation ty, pos, reduced)
+    | Match (te, des, _, pos, reduced) ->
+      Match (te, des, TypedAnnotation ty, pos, reduced)
+
 let set_term_type (te: term) (ty: term) : term =
   match te with
     | Universe (ty, lvl, pos) -> 
@@ -150,6 +176,7 @@ and fv_typeannotation (ty: typeannotation) : IndexSet.t =
   match ty with
     | NoAnnotation -> IndexSet.empty
     | Annotation te -> fv_term te
+    | TypedAnnotation te -> fv_term te
     | Typed te -> fv_term te
   
 
@@ -212,6 +239,7 @@ and bv_typeannotation (ty: typeannotation) : IndexSet.t =
   match ty with
     | NoAnnotation -> IndexSet.empty
     | Annotation te -> bv_term te
+    | TypedAnnotation te -> bv_term te
     | Typed te -> bv_term te
 
 
diff --git a/src/core/kernel/calculus_parser.ml b/src/core/kernel/calculus_parser.ml
index f72822a..d487bec 100644
--- a/src/core/kernel/calculus_parser.ml
+++ b/src/core/kernel/calculus_parser.ml
@@ -436,7 +436,7 @@ let rec parse_definition (defs: defs) (leftmost: int * int) : definition parsing
     DefDefinition (s, 
 		  (set_term_annotation 
 		     (set_term_pos 
-			(build_lambdas qs te) 
+			(build_lambdas qs (set_term_annotation te ty)) 
 			(pos_to_position (startpos2, endpos2))
 		     )
 		     (set_term_pos 
diff --git a/src/core/kernel/calculus_pprinter.ml b/src/core/kernel/calculus_pprinter.ml
index 72de4a5..e08c076 100644
--- a/src/core/kernel/calculus_pprinter.ml
+++ b/src/core/kernel/calculus_pprinter.ml
@@ -23,18 +23,46 @@ type pp_option = {
   show_indices : bool;
   show_position : bool;
   show_univ : bool;
+  show_type: bool;
 }
 
 let pp_option = ref {show_implicit = true; 
 		     show_indices = true; 
 		     show_position = false; 
 		     show_univ = false;
+		     show_type = false;
 		    }
 
 let verbatims (l: name list) = Verbatim (String.concat "" l)
 
 (* transform a term into a box *)
 let rec term2token (vars: name list) (te: term) (p: place): token =
+  match get_term_annotation te with 
+    | Typed ty when !pp_option.show_type ->
+      Box [Verbatim "(";
+	   term2token vars (set_term_noannotation te) Alone; Space 1;
+	   Verbatim "::"; Space 1;
+	   term2token vars ty Alone;
+	   Verbatim ")"
+	  ]
+
+    | Annotation ty when !pp_option.show_type ->
+      Box [Verbatim "(";
+	   term2token vars (set_term_noannotation te) Alone; Space 1;
+	   Verbatim ":?:"; Space 1;
+	   term2token vars ty Alone;
+	   Verbatim ")"
+	  ]
+
+    | TypedAnnotation ty when !pp_option.show_type ->
+      Box [Verbatim "(";
+	   term2token vars (set_term_noannotation te) Alone; Space 1;
+	   Verbatim ":?:"; Space 1;
+	   term2token vars ty Alone;
+	   Verbatim ")"
+	  ]
+
+    | _ ->
   match te with
 
     | Universe (Type, _, _) -> Verbatim "Type"
@@ -252,7 +280,7 @@ let substitution2string (ctxt: context ref) (s: substitution) : string =
 
 let poussin_error2token (err: poussin_error) : token =
   match err with
-    | FreeError s -> Verbatim "FreeError"
+    | FreeError s -> Verbatim s
     | Unshiftable_term _ -> Verbatim "Unshiftable_term"
     | UnknownCste s -> verbatims ["UnknownCste: "; s]
     | NoUnification (ctxt, te1, te2) -> 
@@ -261,10 +289,14 @@ let poussin_error2token (err: poussin_error) : token =
 	   term2token (context2namelist (ref ctxt)) te2 Alone; Newline]
 
     | NoNatureUnification  _ -> Verbatim "NoNatureUnification"
-    | UnknownUnification  _ -> Verbatim "UnknownUnification"
+    | UnknownUnification (ctxt, te1, te2) -> 
+      Box [Verbatim "UnknownUnification between"; Newline; 
+	   term2token (context2namelist (ref ctxt)) te1 Alone; Newline; 
+	   term2token (context2namelist (ref ctxt)) te2 Alone; Newline]
     | NegativeIndexBVar  _ -> Verbatim "NegativeIndexBVar"
     | UnknownBVar  _ -> Verbatim "UnknownBVar"
     | UnknownFVar _ -> Verbatim "UnknownFVar"
+    | NotInductiveDestruction _ -> Verbatim "NotInductiveDestruction"
 	
 let poussin_error2string (err: poussin_error) : string =
   let token = poussin_error2token err in
diff --git a/src/core/kernel/calculus_reduction.ml b/src/core/kernel/calculus_reduction.ml
index 8268415..31e2540 100644
--- a/src/core/kernel/calculus_reduction.ml
+++ b/src/core/kernel/calculus_reduction.ml
@@ -57,108 +57,104 @@ let rec pattern_match (p: pattern) (te: term) : (term list) option =
 *)
 
 let rec reduction_term (defs: defs) (strat: reduction_strategy) (te: term) : term = 
-  match te with
-    | Universe _ | Var _ | AVar _ | TName _ -> te
-
-    | _ when is_reduced te -> te
-
-    | Cste (n, ty, position, _) -> (
-      match strat.delta with
-	(* no unfolding *)
-	| None -> te
-
-	| Some delta -> (
-	  try 
-	    match Hashtbl.find defs n with
-	      (* delta strong -> we return it 
-		 delta_weak -> we make sure the resulting term is 'clean'
-	      *)
-	      | Definition te ->
-		let te' = reduction_term defs strat te in
-		set_reduced (
-		  match delta with
-		    | DeltaStrong -> te'
-		    | DeltaWeak when is_clean_term te' -> te'
-		    | _ -> te
-		)
-	      | _ -> set_reduced te
-	  with
-	    | Not_found -> raise (PoussinException (UnknownCste n))
-	      
-	)
-	  
-    )
-
-    | Lambda _ | Forall _ when strat.beta != Some BetaStrong -> set_reduced te
-
-    | Lambda ((n, ty, nature, pos), te, ty2, pos2, _) ->
-      (
-	let te = reduction_term defs strat te in
-	Lambda ((n, ty, nature, pos), te, ty2, pos2, true)
+  let te' = (
+    match te with
+      | Universe _ | Var _ | AVar _ | TName _ -> te
+
+      | _ when is_reduced te -> te
+
+      | Cste (n, ty, position, _) -> (
+	try 
+	  match Hashtbl.find defs n with
+		(* delta strong -> we return it 
+		   delta_weak -> we make sure the resulting term is 'clean'
+		*)
+	    | Definition te -> (
+	      match strat.delta with
+		| Some _ -> 
+		  let te' = reduction_term defs strat te in
+		  te'
+		| None -> set_reduced te
+	    )
+	    | _ -> set_reduced te
+	with
+	  | Not_found -> raise (PoussinException (UnknownCste n))
+	    
       )
+	
+      | Lambda _ | Forall _ when strat.beta != Some BetaStrong -> set_reduced te
 
-    | Forall ((n, ty, nature, pos), te, ty2, pos2, _) ->
-      (
-	let te = reduction_term defs strat te in
-	Forall ((n, ty, nature, pos), te, ty2, pos2, true)
-      )
+      | Lambda ((n, ty, nature, pos), te, ty2, pos2, _) ->
+	(
+	  let te = reduction_term defs strat te in
+	  Lambda ((n, ty, nature, pos), te, ty2, pos2, true)
+	)
 
-    | Let _ when strat.zeta = false && strat.beta != Some BetaStrong -> set_reduced te
-    | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = false && strat.beta = Some BetaStrong ->
-      Let ((n, te, pos), reduction_term defs strat te2, ty, pos2, true)
+      | Forall ((n, ty, nature, pos), te, ty2, pos2, _) ->
+	(
+	  let te = reduction_term defs strat te in
+	  Forall ((n, ty, nature, pos), te, ty2, pos2, true)
+	)
 
-    | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = true ->
+      | Let _ when strat.zeta = false && strat.beta != Some BetaStrong -> set_reduced te
+      | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = false && strat.beta = Some BetaStrong ->
+	Let ((n, te, pos), reduction_term defs strat te2, ty, pos2, true)
+
+      | Let ((n, te, pos), te2, ty, pos2, _) when strat.zeta = true ->
       (* here we compute the reduction of te and shift it such that it is at the same level as te2 *)
-      let te = shift_term (reduction_term defs strat te) 1 in
+	let te = shift_term (reduction_term defs strat te) 1 in
       (* we substitute all occurence of n by te *)
-      let te2 = term_substitution (IndexMap.singleton 0 te) te2 in
+	let te2 = term_substitution (IndexMap.singleton 0 te) te2 in
       (* and we shift back to the proper level *)
-      let te2 = shift_term te2 (-1) in
-      reduction_term defs strat te2
-
-    | Match _ when strat.iota = false -> set_reduced te
-    | Match (dte, des, ty, pos, _) -> (
-      let dte = reduction_term defs strat dte in
-      let res = fold_stop (fun () (ps, body) ->
-	fold_stop (fun () p ->
-	  match pattern_match p dte with
-	    | None -> Left ()
-	    | Some l ->
+	let te2 = shift_term te2 (-1) in
+	reduction_term defs strat te2
+
+      | Match _ when strat.iota = false -> set_reduced te
+      | Match (dte, des, ty, pos, _) -> (
+	let dte = reduction_term defs strat dte in
+	let res = fold_stop (fun () (ps, body) ->
+	  fold_stop (fun () p ->
+	    match pattern_match p dte with
+	      | None -> Left ()
+	      | Some l ->
 	      (* we will do the same thing as in let, but on the reversed order of the matching list *)
-	      let te = List.fold_left (fun acc te -> 
+		let te = List.fold_left (fun acc te -> 
 		(* rewrite the var 0 *)
-		let acc = term_substitution (IndexMap.singleton 0 te) acc in
+		  let acc = term_substitution (IndexMap.singleton 0 te) acc in
 		(* shift the term by -1 *)
-		let acc = shift_term acc (-1) in
-		acc
-	      ) 
-		body 
-		(List.map (fun te -> shift_term te (List.length l)) (List.rev l)) in
-	      Right te
-	) () ps
-      ) () des in
-      match res with
-	| Left () -> set_reduced te
-	| Right te -> reduction_term defs strat te
-    )
-
-    | App (Lambda ((n, ty, nature, pos), te, ty2, pos2, _), (hd1, hd2)::tl, app_ty, app_pos, _) ->
-      let hd1 = shift_term (reduction_term defs strat hd1) 1 in
-      let f = term_substitution (IndexMap.singleton 0 hd1) te in
-      reduction_term defs strat (App (shift_term f (-1), tl, app_ty, app_pos, false))
-
-    | App (f, [], _, _, _) ->
-      set_reduced (reduction_term defs strat f)
-
-    | App (f, args, ty, pos, _) when not (is_reduced f) -> (
-      let f = reduction_term defs strat f in
-      set_reduced (reduction_term defs strat (App (f, args, ty, pos, false)))
-    )
-
-    | App (f, args, ty, pos, _) when is_reduced f ->
-      let args = List.map (fun (te, n) -> reduction_term defs strat te, n) args in
-      App (f, args, ty, pos, true)
+		  let acc = shift_term acc (-1) in
+		  acc
+		) 
+		  body 
+		  (List.map (fun te -> shift_term te (List.length l)) (List.rev l)) in
+		Right te
+	  ) () ps
+	) () des in
+	match res with
+	  | Left () -> set_reduced te
+	  | Right te -> reduction_term defs strat te
+      )
+
+      | App (Lambda ((n, ty, nature, pos), te, ty2, pos2, _), (hd1, hd2)::tl, app_ty, app_pos, _) ->
+	let hd1 = shift_term (reduction_term defs strat hd1) 1 in
+	let f = term_substitution (IndexMap.singleton 0 hd1) te in
+	reduction_term defs strat (App (shift_term f (-1), tl, app_ty, app_pos, false))
+
+      | App (f, [], _, _, _) ->
+	set_reduced (reduction_term defs strat f)
+
+      | App (f, args, ty, pos, _) when not (is_reduced f) -> (
+	let f = reduction_term defs strat f in
+	set_reduced (reduction_term defs strat (App (f, args, ty, pos, false)))
+      )
 
+      | App (f, args, ty, pos, _) when is_reduced f ->
+	let args = List.map (fun (te, n) -> reduction_term defs strat te, n) args in
+	App (f, args, ty, pos, true)
+  ) in
+  match strat.delta with
+    | Some DeltaWeak when is_clean_term te' -> te'
+    | _ -> set_reduced te      
 
 
 and reduction_typeannotation (defs: defs) (strat: reduction_strategy) (ty: typeannotation) : typeannotation =
diff --git a/src/core/kernel/calculus_substitution.ml b/src/core/kernel/calculus_substitution.ml
index 8607d0f..eaada55 100644
--- a/src/core/kernel/calculus_substitution.ml
+++ b/src/core/kernel/calculus_substitution.ml
@@ -64,7 +64,9 @@ and leveled_shift_term (te: term) (level: int) (delta: int) : term =
 and leveled_shift_typeannotation (ty: typeannotation) (level: int) (delta: int) : typeannotation =
   match ty with
     | NoAnnotation -> NoAnnotation
+      (* this case should be an error ... *)
     | Annotation te -> Annotation (leveled_shift_term te level delta)
+    | TypedAnnotation te -> TypedAnnotation (leveled_shift_term te level delta)
     | Typed te -> Typed (leveled_shift_term te level delta)
 
 and leveled_shift_destructor (des: pattern list * term) (level: int) (delta: int) : pattern list * term =
@@ -135,6 +137,7 @@ and typeannotation_substitution (s: substitution) (ty: typeannotation) : typeann
   match ty with
     | NoAnnotation -> NoAnnotation
     | Annotation te -> Annotation (term_substitution s te)
+    | TypedAnnotation te -> TypedAnnotation (term_substitution s te)
     | Typed te -> Typed (term_substitution s te)
 
 and destructor_substitution (s: substitution) (des: pattern list * term) : pattern list * term =
diff --git a/src/core/kernel/calculus_typecheck.ml b/src/core/kernel/calculus_typecheck.ml
index 1fde787..1bbf7d0 100644
--- a/src/core/kernel/calculus_typecheck.ml
+++ b/src/core/kernel/calculus_typecheck.ml
@@ -72,7 +72,7 @@ let rec flush_fvars (defs: defs) (ctxt: context ref) (l: term list) : term list
     match te with
       | None when not (IndexSet.mem i lfvs) ->
 	(* there is no value for this free variable, and it does not appear in the terms --> remove it *)
-	printf "removed: %s\n" (string_of_int i);
+	(*printf "removed: %s\n" (string_of_int i);*)
 	tl, (terms, fvs)
       | None when IndexSet.mem i lfvs ->
 	(* there is no value for this free variable, but it does appear in the terms --> keep it *)
@@ -105,11 +105,19 @@ let rec flush_fvars (defs: defs) (ctxt: context ref) (l: term list) : term list
   (if List.length !ctxt.bvs != 0 then
       ctxt := { !ctxt with
 	fvs = (fvs @ (List.hd !ctxt.fvs))::(List.tl !ctxt.fvs)
-      });
+      } else 
+      List.iter (fun te -> 
+	if not (IndexSet.is_empty (fv_term te)) then
+	  let msg = String.concat "" ["there are free variables in the remaining term: \n"; term2string ctxt te] in
+	  raise (PoussinException (FreeError msg))
+  
+      ) terms
+  );
   terms
 
 
 let pop_quantification (defs: defs) (ctxt: context ref) (tes: term list) : (name * term * nature * position) * term list =
+  (* we should here flush the bvars, using the conversion_hypothesis *)
   (* we flush the free variables *)
   let tes = flush_fvars defs ctxt tes in
   (* we grab the remaining context and the popped frame *)
@@ -219,6 +227,26 @@ let nature_unify (n1: nature) (n2: nature) : nature option =
     | Explicit, Explicit -> Some Explicit
     | Implicit, Implicit -> Some Implicit
 
+let rec head (te: term) : term =
+  match te with
+    | App (hd, _, _, _, _) ->
+      head hd
+    | _ -> te
+
+let rec pattern_to_term (p: pattern) : term =
+  fst (pattern_to_term_loop p 0)
+and pattern_to_term_loop (p: pattern) (i: int): term * int =
+  match p with
+    | PAvar -> (avar_ (), i)
+    | PName s -> (var_ i, i+1)
+    | PCstor (n, args) ->
+      let args, i = List.fold_left (fun (hds, i) (p, n) ->
+	let p, i = pattern_to_term_loop p i in
+	((hds @ [p, n]), i)
+      ) ([], i) args in
+      (app_ (cste_ n) args, i)
+
+
 let unification_strat = {
   beta = Some BetaWeak;
   delta = Some DeltaStrong;
@@ -235,6 +263,14 @@ let typeinfer_strat = {
   eta = true;
 }
 
+let simplification_strat = {
+  beta = Some BetaWeak;
+  delta = Some DeltaWeak;
+  iota = false;
+  zeta = false;
+  eta = false;
+}
+
 let rec typecheck 
     (defs: defs)
     (ctxt: context ref)
@@ -245,8 +281,14 @@ let rec typecheck
       ignore(unification defs ctxt false ty' ty);
       te
     | Annotation ty' ->
-      (* TODO *)
-      typecheck defs ctxt (set_term_noannotation te) ty
+      let ty' = typecheck defs ctxt ty' (type_ (UName "")) in
+      let te = typeinfer defs ctxt (set_term_tannotation te ty') in
+      ignore(unification defs ctxt false (get_type te) ty);
+      te 
+    | TypedAnnotation ty' ->
+      let te = typeinfer defs ctxt te in
+      ignore(unification defs ctxt false (get_type te) ty);
+      te 
     | NoAnnotation ->
       let te = typeinfer defs ctxt te in
       ignore(unification defs ctxt false (get_type te) ty);
@@ -259,94 +301,164 @@ and typeinfer
     (te: term) : term =
   match get_term_annotation te with
     | Typed ty -> te
+    | Annotation ty ->
+      let ty = typecheck defs ctxt ty (type_ (UName "")) in
+      typeinfer defs ctxt (set_term_tannotation te ty)
     | _ ->
-      match te with
-	| Universe _ -> te
-	| Cste (n, _, pos, reduced) -> (
-	  try 
-	    match Hashtbl.find defs n with
-	      | Inductive (_, ty) | Axiom ty | Constructor ty -> 
-		Cste (n, Typed ty, pos, reduced)
-	      | Definition te -> 
-		Cste (n, Typed (get_type te), pos, reduced)
-	  with
-	    | Not_found -> raise (PoussinException (UnknownCste n))
-	)
+      let te' = (
+	match te with
+	  | Universe _ -> te
+	  | Cste (n, _, pos, reduced) -> (
+	    try 
+	      match Hashtbl.find defs n with
+		| Inductive (_, ty) | Axiom ty | Constructor ty -> 
+		  Cste (n, Typed ty, pos, reduced)
+		| Definition te -> 
+		  Cste (n, Typed (get_type te), pos, reduced)
+	    with
+	      | Not_found -> raise (PoussinException (UnknownCste n))
+	  )
 
-	| Var (i, _, pos) when i < 0 ->
-	  Var (i, Typed (fvar_type ctxt i), pos)
-	| Var (i, _, pos) when i >= 0 ->
-	  Var (i, Typed (bvar_type ctxt i), pos)
+	  | Var (i, _, pos) when i < 0 ->
+	    Var (i, Typed (fvar_type ctxt i), pos)
+	  | Var (i, _, pos) when i >= 0 ->
+	    Var (i, Typed (bvar_type ctxt i), pos)
 
-	| AVar (_, pos) ->
-	  add_fvar ~pos:pos ctxt
+	  | AVar (_, pos) ->
+	    add_fvar ~pos:pos ctxt
 
-	| TName (n, _, pos) -> (
+	  | TName (n, _, pos) -> (
 	  (* we first look for a variable *)
-	  match var_lookup ctxt n with
-	    | Some i -> 
-	      Var (i, Typed (bvar_type ctxt i), pos)
-	    | None -> 
-	      typeinfer defs ctxt (Cste (n, NoAnnotation, pos, false))		
-	)
+	    match var_lookup ctxt n with
+	      | Some i -> 
+		Var (i, Typed (bvar_type ctxt i), pos)
+	      | None -> 
+		typeinfer defs ctxt (Cste (n, NoAnnotation, pos, false))		
+	  )
 
-	| Forall ((s, ty, n, pq), te, _, p, reduced) ->
+	  | Forall ((s, ty, n, pq), te, _, p, reduced) ->
 	  (* first let's be sure that ty :: Type *)
-	  let ty = typecheck defs ctxt ty (type_ (UName "")) in
+	    let ty = typecheck defs ctxt ty (type_ (UName "")) in
 	  (* we push the quantification *)
-	  push_quantification (s, ty, n, pq) ctxt;
+	    push_quantification (s, ty, n, pq) ctxt;
 	  (* we typecheck te :: Type *)
-	  let te = typecheck defs ctxt te (type_ (UName "")) in
+	    let te = typecheck defs ctxt te (type_ (UName "")) in
 	  (* we pop quantification *)
-	  let q1, [te] = pop_quantification defs ctxt [te] in
+	    let q1, [te] = pop_quantification defs ctxt [te] in
 	  (* and we returns the term with type Type *)
-	  Forall ((s, ty, n, pq), te, Typed (type_ (UName "")), p, reduced)
+	    Forall ((s, ty, n, pq), te, Typed (type_ (UName "")), p, reduced)
 
-	| Lambda ((s, ty, n, pq), te, _, p, reduced) ->
+	  | Lambda ((s, ty, n, pq), te, _, p, reduced) ->
 	  (* first let's be sure that ty :: Type *)
-	  let ty = typecheck defs ctxt ty (type_ (UName "")) in
+	    let ty = typecheck defs ctxt ty (type_ (UName "")) in
 	  (* we push the quantification *)
-	  push_quantification (s, ty, n, pq) ctxt;
+	    push_quantification (s, ty, n, pq) ctxt;
 	  (* we typecheck te :: Type *)
-	  let te = typeinfer defs ctxt te in
+	    let te = typeinfer defs ctxt te in
 	  (* we pop quantification *)
-	  let q1, [te] = pop_quantification defs ctxt [te] in
+	    let q1, [te] = pop_quantification defs ctxt [te] in
 	  (* and we returns the term with type Type *)
-	  let res = Forall ((s, ty, n, pq), get_type te, Typed (type_ (UName "")), NoPosition, reduced) in
-	  Lambda ((s, ty, n, pq), te, Typed res, p, reduced)
+	    let res = Forall ((s, ty, n, pq), get_type te, Typed (type_ (UName "")), NoPosition, reduced) in
+	    Lambda ((s, ty, n, pq), te, Typed res, p, reduced)
 
-	| App (hd, [], _, pos, reduced) ->
-	  typeinfer defs ctxt hd 
+	  | App (hd, [], _, pos, reduced) ->
+	    typeinfer defs ctxt hd 
 
-	| App (hd, (arg, n)::args, _, pos, reduced) ->	  
+	  | App (hd, (arg, n)::args, _, pos, reduced) ->	  
 	  (* we infer hd and arg *)
-	  let hd = typeinfer defs ctxt hd in
-	  let arg = typeinfer defs ctxt arg in
+	    let hd = typeinfer defs ctxt hd in
+	    let arg = typeinfer defs ctxt arg in
 	  (* we unify the type of hd with a forall *)
-	  let fty = add_fvar ctxt in
-	  let hd_ty = unification defs ctxt true (get_type hd) (forall_ ~annot:(Typed (type_ (UName ""))) "@typeinfer_App" ~nature:NJoker ~ty:fty (avar_ ())) in
-	  let Forall ((_, _, n', _), _, _, _, _) = hd_ty in
+	    let fty = add_fvar ctxt in
+	    let hd_ty = unification defs ctxt true (get_type hd) (forall_ ~annot:(Typed (type_ (UName ""))) "@typeinfer_App" ~nature:NJoker ~ty:fty (avar_ ())) in
+	    let Forall ((_, _, n', _), _, _, _, _) = hd_ty in
 	  (* if n' is Implicit and n is Explicit, it means we need to insert a free variable *)
-	  if n' = Implicit && n = Explicit then (
-	    let new_arg = add_fvar ctxt in
+	    if n' = Implicit && n = Explicit then (
+	      let new_arg = add_fvar ctxt in
 	    (* and retypeinfer the whole *)
-	    typeinfer defs ctxt (App (hd, (new_arg, n')::(arg, n)::args, NoAnnotation, pos, reduced))
-	  ) else (
+	      typeinfer defs ctxt (App (hd, (new_arg, n')::(arg, n)::args, NoAnnotation, pos, reduced))
+	    ) else (
 	    (* needs to unify the type properly *)
-	    let ty = unification defs ctxt true fty (get_type arg) in
-	    let Forall ((q, _, n', pq), te, Typed fty, p, reduced) = hd_ty in
-	    (* we build a new head, as the reduction of hd and arg, with the proper type *)
-	    let new_hd_ty = reduction_term defs typeinfer_strat (App (Lambda ((q, ty, n, pq), te, Typed fty, p, reduced), (arg,n)::[], Typed fty, pos, false)) in
-	    let new_hd = reduction_term defs typeinfer_strat (
-	      App (hd, (arg, n)::[], 
-		   Typed (new_hd_ty), pos,
-		   false)
-	    ) in 
-	    typeinfer defs ctxt (App (new_hd, args, NoAnnotation, pos, reduced))
-	  )
-	  
-	| _ -> raise (Failure (String.concat "" ["typeinfer: NYI for " ; term2string ctxt te]))
-	  
+	      let ty = unification defs ctxt true fty (get_type arg) in
+	      let Forall ((q, _, n', pq), te, Typed fty, p, reduced) = hd_ty in
+	      (* we build a new head, as the reduction of hd and arg, with the proper type *)
+	      let new_hd_ty = (App (Lambda ((q, ty, n, pq), te, Typed fty, p, reduced), (arg,n)::[], Typed fty, pos, false)) in
+	      (*printf "Unification, App new_hd_ty:\n%s\n\n" (term2string ctxt new_hd_ty);*)
+	      let new_hd_ty = reduction_term defs simplification_strat new_hd_ty in
+	      let new_hd = App (hd, (arg, n)::[], 
+				Typed (new_hd_ty), pos,
+				false) in
+	      (*printf "Unification, App new_hd:\n%s\n\n" (term2string ctxt new_hd);*)
+	      let new_hd = reduction_term defs simplification_strat (
+		new_hd
+	      ) in 
+	      typeinfer defs ctxt (App (new_hd, args, NoAnnotation, pos, reduced))
+	    )
+
+	  | Match (te, des, aty, pos, reduced) ->
+	  (* first we typecheck the destructed term *)
+	    let te = typeinfer defs ctxt te in
+	  (* then we assure ourselves that it is an inductive *)
+	    let tety = reduction_term defs typeinfer_strat (get_type te) in
+	    let _ = 
+	      match head tety with
+		| Cste (n, _, _, _) -> (
+		  try 
+		    match Hashtbl.find defs n with
+		      | Inductive _ as ty -> ty
+		      | _ -> raise (PoussinException (NotInductiveDestruction (!ctxt, te)))
+		  with
+		    | Not_found -> raise (PoussinException (UnknownCste n))
+		)
+		| _ -> raise (PoussinException (NotInductiveDestruction (!ctxt, te)))
+	    in 
+	  (* we create a type for the return value *)
+	    let ret_ty = 
+	      match aty with
+		| TypedAnnotation ty -> ty
+		| _ -> add_fvar ctxt
+	    in
+	  (* then we traverse the destructors *)
+	    let des = List.map (fun (ps, des) ->
+	    (* first grab the vars of the patterns *)
+	      let vars = patterns_vars ps in
+	    (* we push quantification corresponding to the pattern vars *)
+	      List.iter (fun v -> 
+		let ty = add_fvar ctxt in
+		push_quantification (v, ty, Explicit (*dummy*), NoPosition) ctxt
+	      ) vars;
+	    (* we need to shift ret_ty, te, and tety to be at the same level *)
+	      let ret_ty = shift_term ret_ty (List.length vars) in
+	      let tety = shift_term tety (List.length vars) in
+	      let te = shift_term te (List.length vars) in
+	    (* then we create the terms corresponding to the patterns *)
+	      let tes = List.map (fun p -> pattern_to_term p) ps in
+	    (* then, for each patterns, we typecheck against tety *)
+	      let tes = List.map (fun te -> typecheck defs ctxt te tety) tes in
+	    (* then, for each pattern *)
+	      let des = List.map (fun hd ->
+	      (* we unify it (with negative polarity) with te *)
+		let _ = unification defs ctxt false hd te in
+	      (* and typecheck des against ret_ty *)
+		typecheck defs ctxt des ret_ty
+	      ) tes in
+	    (* we pop all quantifiers *)
+	      let _, des = pop_quantifications defs ctxt des (List.length vars) in
+	    (* and finally returns all the constructors *)
+	      List.map2 (fun hd1 hd2 -> [hd1], hd2) ps des
+	    ) des in
+	    let ret_ty = typecheck defs ctxt ret_ty (type_ (UName "")) in
+	    Match (te, List.concat des, Typed ret_ty, pos, reduced)
+	      
+	      
+	  | _ -> raise (Failure (String.concat "" ["typeinfer: NYI for " ; term2string ctxt te]))
+      ) in (*
+      match get_term_annotation te with
+	| TypedAnnotation ty ->
+	  let ty = unification defs ctxt true (get_type te') ty in
+	  set_term_type te' ty
+	| _ ->*) te'
+
 and unification 
     (defs: defs)
     (ctxt: context ref)
@@ -475,12 +587,14 @@ and unification
       (* and we return the term *)
       Let ((s, ty, pq), te, Typed lty, p1, false)
 
+	(*
     (* TODO: App case *)
     (* some higher order unification *)
     | App (Var (i, _, _), _::args, _, _, true), t2 when i < 0 ->
       raise (Failure "unification: NYI")
     | t1, App (Var (i, _, _), _::args, _, _, true) when i < 0  ->
       raise (Failure "unification: NYI")
+	*)
     (* the case of two application: with the same arity *)
     | App (hd1, args1, Typed ty1, pos1, true), App (hd2, args2, Typed ty2, pos2, true) when List.length args1 = List.length args2 ->
       let ty = unification defs ctxt polarity ty1 ty2 in
@@ -494,6 +608,8 @@ and unification
 	 ) args1 args2) in
       App (hd, args, Typed ty, pos1, false)
 
+    (* *)
+
     (* maybe we can reduce the term *)
     | _ when not (is_reduced te1) ->
       unification defs ctxt polarity (reduction_term defs unification_strat te1) te2
diff --git a/tests/testregression.ml b/tests/testregression.ml
index d85f1f5..bdd0357 100644
--- a/tests/testregression.ml
+++ b/tests/testregression.ml
@@ -70,12 +70,18 @@ let parse_and_typecheck_from_string (str: string) : unit  =
 	let ty = typeinfer defs ctxt ty in
 	let [ty] = flush_fvars defs ctxt [ty] in 
 	Hashtbl.add defs n (Inductive ([], ty));
-	printf "%s: %s\n" n (term2string ctxt ty)
+	printf "-------------------------------------------\n%s: %s\n\n" n (term2string ctxt ty)
       | DefConstructor (n, ty) -> 
 	let ty = typeinfer defs ctxt ty in
 	let [ty] = flush_fvars defs ctxt [ty] in 
 	Hashtbl.add defs n (Constructor ty);
-	printf "%s: %s\n" n (term2string ctxt ty)
+	printf "-------------------------------------------\n%s: %s\n\n" n (term2string ctxt ty)
+      | DefDefinition (n, te) -> 
+	printf "-------------------------------------------\n%s:= %s\n\n" n (term2string ctxt te);
+	let te = typeinfer defs ctxt te in
+	let [te] = flush_fvars defs ctxt [te] in 
+	Hashtbl.add defs n (Definition te);
+	printf "-------------------------------------------\n%s:= %s : %s \n\n" n (term2string ctxt te) (term2string ctxt (get_type te))
       | _ -> raise (Failure "parse_and_typecheck_from_string: NYI")
 
   with
@@ -104,5 +110,8 @@ let defs = ["Inductive True : Prop";
 	    "Constructor eq_refl {A} (a: A): eq a a";
 	    "Inductive ReflexiveRel : Set";
 	    "Constructor build_ReflexiveRel: (A: Set) -> (rel: A -> A -> Prop) -> (refl: (x: A) -> rel x x) -> ReflexiveRel";
-	    "Definition ReflexiveRel_t {rel: ReflexiveRel} : Set :=  match rel with | build_ReflexiveRel A _ _ := A end"
+	    "Definition ReflexiveRel_t {rel: ReflexiveRel} : Set :=  match rel with | build_ReflexiveRel A _ _ := A end";
+	    "Definition ReflexiveRel_rel {rel: ReflexiveRel} : ReflexiveRel_t {rel} -> ReflexiveRel_t {rel} -> Prop := match rel with  | build_ReflexiveRel _ rel _ := rel end";
+	    "Definition ReflexiveRel_refl {rel: ReflexiveRel} : (x: ReflexiveRel_t {rel}) -> ReflexiveRel_rel x x := match rel with  | build_ReflexiveRel _ _ refl := refl  end"
+
 	   ] in List.map (fun def -> parse_and_typecheck_from_string def) defs;;