X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic%2FcicPushParser.ml;h=f9f14df106b971a457c2f10fbed7841bf6ab2c46;hb=2e8243f12626854bdc1e06f2e3d9160ff7901bd3;hp=a76105deb6ed5a651760d5b37e321b29e812c0ac;hpb=8d1c6f47f6a17cae4cc738987184b37e640b48ed;p=helm.git

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index a76105deb..f9f14df10 100644
--- a/helm/ocaml/cic/cicPushParser.ml
+++ b/helm/ocaml/cic/cicPushParser.ml
@@ -611,6 +611,8 @@ let end_element ctxt tag =
             mk_obj_attributes (`Class `Projection :: acc) tl
         | ("class", "elimProp") :: tl ->
             mk_obj_attributes (`Class (`Elim Cic.Prop) :: acc) tl
+        | ("class", "elimCProp") :: tl ->
+            mk_obj_attributes (`Class (`Elim Cic.CProp) :: acc) tl
         | ("class", "elimSet") :: tl ->
             mk_obj_attributes (`Class (`Elim Cic.Set) :: acc) tl
         | ("class", "elimType") :: tl ->