- helena: the improved attribute system allows to export the sorts of Pi's

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

diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index 13e9ce334aee99802cd3ca0ff7bed2401674baed..53956d932ba79185dd03c88657afcfa1ca6d3734 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -87,10 +87,11 @@ let rec out_term st p e och = function
       let op, cp = if p then "(", ")" else "", "" in
       let a = R.alpha B.mem e a in
       let ee = B.push e B.empty a (B.abst n w) in
-      let binder = match N.to_string st n with
-         | "1" -> "Π"
-         | "2" -> "λ"
-         | _   -> ok := false; "?"
+      let binder = match N.to_string st n, a.E.n_sort with
+         | "1", 0 -> "Π"
+         | "1", 1 -> "∀"
+         | "2", _ -> "λ"
+         | _      -> ok := false; "?"
       in
       P.fprintf och "%s%s%a:%a.%a%s"
          op binder out_name a (out_term st false e) w (out_term st false ee) t cp
@@ -109,20 +110,17 @@ let open_out fname =
    let path = F.concat dir fname in
    let och = open_out (path ^ ext) in
    out_preamble och;
-   out_top_comment och (P.sprintf "This file is generated by %s: do not edit" G.version_string);
+   out_top_comment och (P.sprintf "This file was generated by %s: do not edit" G.version_string);
    out_include och "basics/pts";
    och
 
 let output_entity st och (_, na, s, b) =
-   let f i =
-      out_comment och (P.sprintf "notion %u" i);
-      match b with
-         | E.Abbr t ->
-            P.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
-         | E.Abst t ->
-            P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
-         | E.Void   -> C.err ()
-   in
-   E.apix C.err f na
+   out_comment och (P.sprintf "constant %u" na.E.n_apix);
+   match b with
+      | E.Abbr t ->
+         P.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+      | E.Abst t ->
+         P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+      | E.Void   -> C.err ()
 
 let close_out och = close_out och