- Coq/preamble: missing alias added

[helm.git] / helm / software / components / acic_procedural / proceduralHelpers.ml

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 5807e185ae6a4bb2e2313b8a0c36fc9878c9eed3..a9fa6473f280ac7e12fc50422181b99cf0a248cf 100644 (file)
--- 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