X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUtil.ml;h=496452a87bf75f02efaa3344a3742f4592d29406;hb=3f676ab6acafa32514a44bc84d287f44dbc5389e;hp=31b47f672a4b8f7a2a7262d6159e970ed039386d;hpb=fdea894deb3813f1103b0607b5e3854d501d82da;p=helm.git

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 31b47f672..496452a87 100644
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -209,6 +209,8 @@ let attributes_of_obj = function
   | Cic.InductiveDefinition (_, _, _, attributes) ->
       attributes
 
+let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
+
 let arity_of_composed_coercion obj =
   let attrs = attributes_of_obj obj in
   try
@@ -218,6 +220,20 @@ let arity_of_composed_coercion obj =
     | _-> assert false 
   with Not_found -> 0
 ;;
+
+let projections_of_record obj uri =
+  let attrs = attributes_of_obj obj in
+  try
+    let tag=List.find (function `Class (`Record _) -> true|_->false) attrs in
+    match tag with
+    |  `Class (`Record l) -> 
+         List.map (fun (name,_,_) ->
+           let buri = UriManager.buri_of_uri uri in
+           let puri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
+           puri) l
+    | _-> assert false 
+  with Not_found -> []
+;;
       
 let rec mk_rels howmany from =
   match howmany with