X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcomplete_rg%2FcrgOutput.ml;h=3634f9e80171e01ddb7b9ca0fa55973d41c7b13d;hb=4efe53bc2098939c255d5b03941212549f89a1bd;hp=ecc4a33b14aa0b2d37cea29d7b8ba479652d7888;hpb=da715664068e859d20ab81fd6969e64d58c0f57e;p=helm.git

diff --git a/helm/software/lambda-delta/complete_rg/crgOutput.ml b/helm/software/lambda-delta/complete_rg/crgOutput.ml
index ecc4a33b1..3634f9e80 100644
--- a/helm/software/lambda-delta/complete_rg/crgOutput.ml
+++ b/helm/software/lambda-delta/complete_rg/crgOutput.ml
@@ -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
@@ -128,7 +129,7 @@ and exp_bind e a b out tab =
    let a, ns = Y.get_names f a in 
    match b with
       | D.Abst ws ->
-         let e = D.push_bind C.start e a (D.Abst []) in
+	 let e = D.push_bind C.start e a (D.Abst []) in
 	 let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
          X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
       | D.Abbr vs ->