- Procedural convertible rewrites in the conclusion are now detected and replaced...

[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 65d5f1edf14911a93c66c81fdba2cdaf25d71809..e73ccfe596b0b65936fb71f7699b8f82093f9498 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -219,6 +219,10 @@ let convert g ity k predicate =
 let mk_pattern psno ity predicate =
    clear_absts (convert (generalize psno) ity) psno 0 predicate 
 
+let beta v = function
+   | C.ALambda (_, _, _, t) -> subst 1 v t
+   | _                      -> assert false
+
 let get_clears c p xtypes = 
    let meta = C.Implicit None in
    let rec aux c names p it et = function