]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/complete_rg/crgOutput.ml
- we added a parser for lambda-delta textual syntax (file extension .hln)
[helm.git] / helm / software / lambda-delta / complete_rg / crgOutput.ml
index ecc4a33b14aa0b2d37cea29d7b8ba479652d7888..593074ad832a68b54ff19d93b223cdb34b5b0280 100644 (file)
@@ -25,7 +25,8 @@ let pp_attrs out a =
       | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
       | Y.Apix i          -> out (P.sprintf "+%i;" i)
       | Y.Mark i          -> out (P.sprintf "@%i;" i)
-      | Y.Priv            -> out (P.sprintf "%s;" "~") 
+      | Y.Meta s          -> out (P.sprintf "\"%s\";" s)
+      | Y.Priv            -> out (P.sprintf "%s;" "~")
    in
    List.iter map a
 
@@ -71,7 +72,7 @@ let list_rev_iter map e ns l out tab =
            pp_lenv print_string e; print_string " |- "; 
           pp_term print_string hd; print_newline ();
 *)
-          map e hd out tab; f (D.push2 C.err C.start e n ~t:hd)
+          map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
        in
        aux err f e (ns, tl) 
       | _                 -> err ()
@@ -91,7 +92,7 @@ let rec exp_term e t out tab = match t with
       let a =
          let err _ = a in
          let f s = Y.Name (s, true) :: a in
-        H.get_sort err f l
+        H.string_of_sort err f l
       in
       let attrs = [X.position l; X.name a] in
       X.tag X.sort attrs out tab