X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicParser.ml;h=3962323a18767d0faa087f486b44d768cbfa901e;hb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;hp=30e7a0b38903385fdee48dee1dbc28a0458e4467;hpb=b7aefa8f362d07bf9042f6879252345e69da07c8;p=helm.git

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 30e7a0b38..3962323a1 100644
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -694,13 +694,6 @@ let end_element ctxt tag =
       let class_modifiers = pop_class_modifiers ctxt in
       push ctxt
         (match pop_tag_attrs ctxt with
-        | ["value", "coercion"] -> Obj_class (`Coercion 0)
-        | ("value", "coercion")::["arity",n]  
-        | ("arity",n)::["value", "coercion"] -> 
-            let arity = try int_of_string n with Failure _ ->
-              parse_error "\"arity\" must be an integer"
-            in
-            Obj_class (`Coercion arity)
         | ["value", "elim"] ->
             (match class_modifiers with
             | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)