X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicPushParser.ml;fp=helm%2Focaml%2Fcic%2FcicPushParser.ml;h=f9f14df106b971a457c2f10fbed7841bf6ab2c46;hb=2e8243f12626854bdc1e06f2e3d9160ff7901bd3;hp=a76105deb6ed5a651760d5b37e321b29e812c0ac;hpb=cb379a463ec772df8855310fc9bf7276ea5f3f3d;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 ->