X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;fp=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=b2f73f311a9d932374fb4694432c6be0a2469469;hb=70660e05baa914569c52555230901d5a8dd92f0b;hp=3628e5944b93a4708fd2e4fc6ae98bde8e5d6789;hpb=d3548c16f481b14ce94e64c790bc767c59590050;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 3628e5944..b2f73f311 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -335,3 +335,10 @@ let acic_bc c t =
       | t -> t
    in 
    bc c t
+
+let is_acic_proof sorts context v =
+   let id = Ut.id_of_annterm v in
+   try match Hashtbl.find sorts id with
+      | `Prop -> true
+      | _     -> false
+   with Not_found -> is_proof context (cic v)