]> matita.cs.unibo.it Git - helm.git/commitdiff
handles "elimCProp" value for class attribute
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 7 Jun 2005 17:21:08 +0000 (17:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 7 Jun 2005 17:21:08 +0000 (17:21 +0000)
helm/ocaml/cic/cicPushParser.ml

index a76105deb6ed5a651760d5b37e321b29e812c0ac..f9f14df106b971a457c2f10fbed7841bf6ab2c46 100644 (file)
@@ -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 ->