- | E.Abbr t ->
- KP.fprintf och "Definition %a := %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
- | E.Abst t ->
- KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+(*
+ | E.Abbr (B.Cast (w, v)) ->
+ KP.fprintf och "Definition %a : %a.\n%!" out_uri u (out_term st false B.empty) w;
+ KP.fprintf och "exact %a.\n%!" (out_term st true B.empty) v;
+ KP.fprintf och "Time Defined.\n\n%!";
+*)
+ | E.Abbr v ->
+ KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v;
+(* KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok
+ | E.Abst w ->
+ KP.fprintf och "Axiom %a : %a.\n\n%!" out_uri u (out_term st false B.empty) w; !ok