X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgGallina.ml;h=7346e58357c71dcacaadcf5ba5162e48db37804c;hb=fdb80b08af83b86759833142456ce3c4f84cd80e;hp=bc65fe0752244f0c89c737f76c62f325baa57db1;hpb=849001febdebe045a1309e6c2c854e421e6e476b;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml
index bc65fe075..7346e5835 100644
--- a/helm/software/helena/src/basic_rg/brgGallina.ml
+++ b/helm/software/helena/src/basic_rg/brgGallina.ml
@@ -118,6 +118,12 @@ let close_out och () = close_out och
 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