BIG FAT COMMIT REGARDING COERCIONS:

[helm.git] / components / cic / cicUtil.ml

diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml
index de796910a5c7432a410470a3579a094234d6e782..6e07a4995d8ed5d436f43138a1374123b6f79f65 100644 (file)
--- 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 -> []