- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[helm.git] / helm / software / helena / src / basic_rg / brgGallina.ml

diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml
index caa8ab4650b47cc27c1c240289d693ed600c3bf5..bdb78144ac1152bf2f1f24b7e2f7f36af920779e 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgGallina.ml
+++ b/helm/software/helena/src/basic_rg/brgGallina.ml
@@ -111,13 +111,14 @@ let rec out_term st p e och = function
 
 let close_out och () = close_out och
 
-let output_entity och st (_, na, s, b) =
+let output_entity och st (_, na, u, b) =
    out_comment och (KP.sprintf "constant %u" na.E.n_apix);
    match b with
-      | 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 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
       | E.Void   -> C.err ()
 
 (* Interface functions ******************************************************)
@@ -128,5 +129,4 @@ let open_out fname =
    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_include och "basics/pts"; *)
    output_entity och, close_out och