List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
(* let's check if the types of the inductive constructors are well formed. *)
let len = List.length tyl in
List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
(* let's check if the types of the inductive constructors are well formed. *)
let len = List.length tyl in