X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=a9fa6473f280ac7e12fc50422181b99cf0a248cf;hb=4573f1fecaf83f4706f39702555d5319d132477b;hp=5807e185ae6a4bb2e2313b8a0c36fc9878c9eed3;hpb=0b76904a3f10bfd6390d26172fd6979626bd72f4;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 5807e185a..a9fa6473f 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -127,12 +127,15 @@ let get_tail c t =
       | (_, hd) :: _, _ -> hd
       | _               -> assert false
 
-let is_proof c t =
-   match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
+let is_prop c t =
+   match get_tail c (get_type "is_prop" c t) with
       | C.Sort C.Prop -> true
       | C.Sort _      -> false
       | _             -> assert false 
 
+let is_proof c t =
+   is_prop c (get_type "is_prop" c t)
+
 let is_sort = function
    | C.Sort _ -> true
    | _        -> false