Don't cast for check directive

printer.ml

@@ -107,7 +107,7 @@ let print_line out_fmter = function
       print_term def
   | Tcheck (t, ty) ->
     Format.fprintf out_fmter "@[#CHECK %a,@ dk_obj.Expr@ (%a).@]@\n"
-      print_term (Tcast (t, infer t, ty))
+      print_term t
       print_ty ty
   | Tnorm t ->
     Format.fprintf out_fmter "@[#SNF %a.@]@\n"

typer.ml

@@ -209,11 +209,7 @@ let type_line = function
   | Stypedef (a, ty) -> Ttypedef (a, ty)
   | Svardef (id, ty, def) -> Tvardef (id, ty, type_term [] def)
   | Scheck (t, ty) ->
-    let tt = type_term [] t in
-    if subtype (infer tt) ty then
-      Tcheck (tt, ty)
-    else
-      raise Check_failed
+    let tt = type_check [] t ty in Tcheck (tt, ty)
   | Snorm t -> Tnorm (type_term [] t)
 
 let type_check = List.map type_line