added attribute support (not yet in the parser)

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

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 5e0d6d4a94869989f6b9012a06d070caa2672413..f2ea4171bf356923effb70662b800f757f778c32 100644 (file)
--- 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
+