X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralConversion.ml;h=67b293393dbb9cba2e86c7e9c3f1dfee5733f392;hb=6b3242efcd29ea188ef09b445985abb06c5fad3a;hp=97e32b94a458f1cdd3ce9bf9c49f30a21c5c675a;hpb=916c558005ed665c62699a7a4c5347870c8a3efb;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index 97e32b94a..67b293393 100644
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -244,8 +244,9 @@ let elim_inferred_type context goal arg using cpattern =
    let metasenv, ugraph = [], Un.default_ugraph in
    let ety = H.get_type "elim_inferred_type" context using in
    let _splits, args_no = PEH.split_with_whd (context, ety) in
-   let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim 
-      ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no
+   let _metasenv, _subst, predicate, _arg, actual_args = 
+     PT.mk_predicate_for_elim 
+     ~context ~metasenv ~subst:[] ~ugraph ~goal ~arg ~using ~cpattern ~args_no
    in
    let ty = C.Appl (predicate :: actual_args) in
    let upto = List.length actual_args in