X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=e73ccfe596b0b65936fb71f7699b8f82093f9498;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=65d5f1edf14911a93c66c81fdba2cdaf25d71809;hpb=8ed18544e1591dd3068e2d9095b05d0c4349209c;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 65d5f1edf..e73ccfe59 100644
--- 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