let ok = ref true
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
let base = "coq"
let ext = ".v"
let output_entity och st (_, na, u, b) =
out_comment och (KP.sprintf "constant %u" na.E.n_apix);
match b with
+(*
+ | 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
let path = KF.concat dir fname in
let och = open_out (path ^ ext) in
out_preamble och;
- out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+ out_top_comment och version;
output_entity och, close_out och
END