]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUtil.ml
added oblivion_universe and used it in paxck_coercions
[helm.git] / helm / software / components / cic / cicUtil.ml
index 31b47f672a4b8f7a2a7262d6159e970ed039386d..496452a87bf75f02efaa3344a3742f4592d29406 100644 (file)
@@ -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