]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicParser.ml
Big commit to let Ferruccio try the merge_coercion patch.
[helm.git] / helm / ocaml / cic / cicParser.ml
index d81521f99e335e18b77ca2d20092298e3b646ae0..68f1257d1557c3933caaf80825552b0e411834c9 100644 (file)
@@ -686,7 +686,13 @@ let end_element ctxt tag =
             let fields =
               List.map
                 (function
-                  | Obj_field name -> name
+                  | Obj_field name -> 
+                      (match Str.split (Str.regexp " ") name with
+                      | [name] -> name, false
+                      | [name;"coercion"] -> name,true
+                      | _ -> 
+                          parse_error
+                            "wrong \"field\"'s name attribute")
                   | _ ->
                       parse_error
                         "unexpected extra content for \"record\" object class")