X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fxml%2FxmlCrg.ml;h=45e33178a4ffacc651b4f1eb897e80e6326d36b1;hb=e7f64fe2cc67f3514131c8831f87311ff600d005;hp=3eea8cd8724104d162743ac45949a211712a515d;hpb=f7988fc51f7c96617aa2b3320628645480af681a;p=helm.git

diff --git a/helm/software/lambda-delta/src/xml/xmlCrg.ml b/helm/software/lambda-delta/src/xml/xmlCrg.ml
index 3eea8cd87..45e33178a 100644
--- a/helm/software/lambda-delta/src/xml/xmlCrg.ml
+++ b/helm/software/lambda-delta/src/xml/xmlCrg.ml
@@ -32,7 +32,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 ~attr:n ~t:hd ())
 	in
 	aux err f e (ns, tl) 
       | _                 -> err ()
@@ -91,11 +91,11 @@ and exp_bind e a b out tab =
    let a, ns = Y.get_names f a in 
    match b with
       | D.Abst (n, ws) ->
-	 let e = D.push_bind C.start e a (D.Abst (n, ws)) in
+	 let e = D.push_bind C.start e a (D.Abst (n, [])) in
 	 let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
          XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
       | D.Abbr vs      ->
-         let e = D.push_bind C.start e a (D.Abbr vs) in
+         let e = D.push_bind C.start e a (D.Abbr []) in
          let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
          XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
       | D.Void n       ->