X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUtil.ml;h=f2ea4171bf356923effb70662b800f757f778c32;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=5e0d6d4a94869989f6b9012a06d070caa2672413;hpb=b24d13c4dcc96a204951857ddfa18c5ded4cecd0;p=helm.git

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 5e0d6d4a9..f2ea4171b 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -253,3 +253,17 @@ let rec strip_prods n = function
   | Cic.Prod (_, _, tgt) when n > 0 -> strip_prods (n-1) tgt
   | _ -> failwith "not enough prods"
 
+let params_of_obj = function
+  | Cic.Constant (_, _, _, params, _)
+  | Cic.Variable (_, _, _, params, _)
+  | Cic.CurrentProof (_, _, _, _, params, _)
+  | Cic.InductiveDefinition (_, params, _, _) ->
+      params
+
+let attributes_of_obj = function
+  | Cic.Constant (_, _, _, _, attributes)
+  | Cic.Variable (_, _, _, _, attributes)
+  | Cic.CurrentProof (_, _, _, _, _, attributes)
+  | Cic.InductiveDefinition (_, _, _, attributes) ->
+      attributes
+