prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic / cicPushParser.ml

diff --git a/helm/ocaml/cic/cicPushParser.ml b/helm/ocaml/cic/cicPushParser.ml
index a76105deb6ed5a651760d5b37e321b29e812c0ac..f9f14df106b971a457c2f10fbed7841bf6ab2c46 100644 (file)
--- 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 ->