]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicPushParser.ml
The `Record class now records also the name of the fields
[helm.git] / helm / ocaml / cic / cicPushParser.ml
index f9f14df106b971a457c2f10fbed7841bf6ab2c46..3051fb81fa3b0a0c18b15f7173ba0f44d23dc0e1 100644 (file)
@@ -606,7 +606,7 @@ let end_element ctxt tag =
         | ("class", "coercion") :: tl ->
             mk_obj_attributes (`Class `Coercion :: acc) tl
         | ("class", "record") :: tl ->
-            mk_obj_attributes (`Class `Record :: acc) tl
+            mk_obj_attributes (`Class (`Record []) :: acc) tl
         | ("class", "projection") :: tl ->
             mk_obj_attributes (`Class `Projection :: acc) tl
         | ("class", "elimProp") :: tl ->