]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/xml/xmlCrg.ml
the old intermediate language (meta) is now obsolete
[helm.git] / helm / software / lambda-delta / src / xml / xmlCrg.ml
index 3eea8cd8724104d162743ac45949a211712a515d..45e33178a4ffacc651b4f1eb897e80e6326d36b1 100644 (file)
@@ -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       ->