Several bugs fixed:

[helm.git] / components / cic / cicParser.ml

diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml
index 3122affd429fdaa1c25ee141c849d84026e2d9b2..49a5a1ab7cc5d3c48e6a9b9a15a04aca4d0f122f 100644 (file)
--- a/components/cic/cicParser.ml
+++ b/components/cic/cicParser.ml
@@ -667,6 +667,7 @@ let end_element ctxt tag =
       push ctxt 
         (match pop_tag_attrs ctxt with
         | [ "value", "definition"] -> Obj_flavour `Definition
+        | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition
         | [ "value", "fact"] -> Obj_flavour `Fact
         | [ "value", "lemma"] -> Obj_flavour `Lemma
         | [ "value", "remark"] -> Obj_flavour `Remark