From a7c501b62c6d05350b4a98384f85aa35695f2ab8 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 27 Jul 2005 07:53:31 +0000
Subject: [PATCH] added id_of_annterm: Cic.annterm -> Cic.id

---
 helm/ocaml/cic/cicUtil.ml  | 20 ++++++++++++++++++++
 helm/ocaml/cic/cicUtil.mli |  2 ++
 2 files changed, 22 insertions(+)

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 8de1ce2a2..7269e1f84 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -225,5 +225,25 @@ let profile =
       ("!! TOTAL TIME SPENT IN " ^ s ^ ": " ^ string_of_float !total));
   profile
 
+let id_of_annterm =
+  function
+  | Cic.ARel (id,_,_,_)
+  | Cic.AVar (id,_,_)
+  | Cic.AMeta (id,_,_)
+  | Cic.ASort (id,_)
+  | Cic.AImplicit (id,_)
+  | Cic.ACast (id,_,_)
+  | Cic.AProd (id,_,_,_)
+  | Cic.ALambda (id,_,_,_)
+  | Cic.ALetIn (id,_,_,_)
+  | Cic.AAppl (id,_)
+  | Cic.AConst (id,_,_)
+  | Cic.AMutInd (id,_,_,_)
+  | Cic.AMutConstruct (id,_,_,_,_)
+  | Cic.AMutCase (id,_,_,_,_,_)
+  | Cic.AFix (id,_,_)
+  | Cic.ACoFix (id,_,_) -> id
+
   (** WARNING: COMMENT THIS TO ENABLE PROFILING **)
 let profile _ = let profile f x = f x in profile
+
diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index 31c7e4dee..cad3abbee 100644
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -50,6 +50,8 @@ val pack: Cic.term list -> Cic.term
 val unpack: Cic.term -> Cic.term list
 *)
 
+val id_of_annterm: Cic.annterm -> Cic.id
+
 (** {2 Cic selectors} *)
 
 val params_of_obj: Cic.obj -> UriManager.uri list
-- 
2.39.2