Several bugs fixed:

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

diff --git a/components/cic/cic.ml b/components/cic/cic.ml
index c5a5c1e4079991118daf4110fa7fef1c8a785c62..1b02df3f1a12c7367a64a64cdc49fad3f7d1d9c0 100644 (file)
--- a/components/cic/cic.ml
+++ b/components/cic/cic.ml
@@ -57,6 +57,7 @@ type name =
 
 type object_flavour =
   [ `Definition
+  | `MutualDefinition
   | `Fact
   | `Lemma
   | `Remark