some improvements

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

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 4e43164cb0c0b5694b87e09167c81cad2c18390e..b3ce560707348f38f7bd9de27306bd0cc3dc6bdc 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -65,12 +65,6 @@ let rec list_sub start length = function
 
 (* proof construction *******************************************************)
 
-let rec need_whd i = function
-   | C.ACast (_, t, _)               -> need_whd i t
-   | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
-   | _                    when i > 0 -> true
-   | _                               -> false
-
 let lift k n =
    let rec lift_xns k (uri, t) = uri, lift_term k t
    and lift_ms k = function