Added option datatype. Required (for technicalities/Setoids.ma).

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

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 150fe4ad983f6dab3bad1d117877e6093531b755..3122affd429fdaa1c25ee141c849d84026e2d9b2 100644 (file)
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -716,7 +716,8 @@ let end_element ctxt tag =
             in
             Obj_class (`Record fields)
         | ["value", "projection"] -> Obj_class `Projection
-        | _ -> attribute_error ())
+        | ["value", "inversion"] -> Obj_class `InversionPrinciple
+       | _ -> attribute_error ())
   | tag ->
       match find_helm_exception ctxt with
       | Some (exn, arg) -> raise (Getter_failure (exn, arg))