X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2FcicUtil.ml;h=6e07a4995d8ed5d436f43138a1374123b6f79f65;hb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;hp=de796910a5c7432a410470a3579a094234d6e782;hpb=f764844fa35ab0bb9c10707151340b924060f069;p=helm.git

diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index de796910a..6e07a4995 100644
--- a/components/cic/cicUtil.ml
+++ b/components/cic/cicUtil.ml
@@ -207,6 +207,17 @@ let attributes_of_obj = function
   | Cic.CurrentProof (_, _, _, _, _, attributes)
   | Cic.InductiveDefinition (_, _, _, attributes) ->
       attributes
+
+let arity_of_composed_coercion obj =
+  let attrs = attributes_of_obj obj in
+  try
+    let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
+    match tag with
+    |  `Class (`Coercion n) -> n
+    | _-> assert false 
+  with Not_found -> 0
+;;
+      
 let rec mk_rels howmany from =
   match howmany with 
   | 0 -> []