]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUtil.ml
changed default parameter values...
[helm.git] / helm / ocaml / cic / cicUtil.ml
index d3fcffd8039235c101bd850492d7a7b55c4be082..7269e1f843dcdba470e4af8b4ee66cd45b8f8b27 100644 (file)
@@ -224,3 +224,26 @@ let profile =
      print_endline
       ("!! 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
+