]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/xml/xmlCrg.ml
new syntax of abstractions propagated to complete_rg
[helm.git] / helm / software / helena / src / xml / xmlCrg.ml
index 535682143652841bf7a7fcedd5b314eaf386ee52..f04930851035d2d323499eef96a046e0477a5f2d 100644 (file)
@@ -80,13 +80,13 @@ and exp_appl st e a v out tab =
    XL.tag XL.appl attrs ~contents:(exp_term st e v) out tab;
 
 and exp_bind st e a b out tab = match b with
-   | D.Abst (n, w) ->
+   | D.Abst (_, n, w) ->
       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      ->
+   | D.Abbr v         ->
       let attrs = [XL.name a] in
       XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
-   | D.Void        ->
+   | D.Void           ->
       let attrs = [XL.name a] in
       XL.tag XL.void attrs out tab