Inductive definitions are now interpreted (but records are not interpreted yet).

[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 97e32b94a458f1cdd3ce9bf9c49f30a21c5c675a..67b293393dbb9cba2e86c7e9c3f1dfee5733f392 100644 (file)
--- 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