]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlCrg.ml
- we are moving from old (patched) management of sort inclusion
[helm.git] / helm / software / helena / src / xml / xmlCrg.ml
index 311a0b4a1192c3a076dc2dd4a17472b9148c504f..535682143652841bf7a7fcedd5b314eaf386ee52 100644 (file)
@@ -81,7 +81,7 @@ and exp_appl st e a v out tab =
 
 and exp_bind st e a b out tab = match b with
    | D.Abst (n, w) ->
-      let attrs = [XL.level st n; XL.name a; XL.kind a] in
+      let attrs = [XL.layer st n; XL.name a; XL.kind a] in
       XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
    | D.Abbr v      ->
       let attrs = [XL.name a] in