X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_procedural%2FproceduralMode.ml;h=e13846fc85a3ddee2b6dbb4f805be0ab7fac1de6;hb=cd85befa31c33698c57d5d5d0d7a2384bb2644f9;hp=d2ddc6c9847c37d0c25dba76cc9a4dde0c9de096;hpb=2a39b3fe15889f379932c642f4775a5f8e756022;p=helm.git

diff --git a/components/acic_procedural/proceduralMode.ml b/components/acic_procedural/proceduralMode.ml
index d2ddc6c98..e13846fc8 100644
--- a/components/acic_procedural/proceduralMode.ml
+++ b/components/acic_procedural/proceduralMode.ml
@@ -51,7 +51,7 @@ let bkd c t =
    let classes, rc = Cl.classify c t in
    let premises, _ = PEH.split_with_whd (c, t) in
    match rc with
-      | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true
+      | Some (i, j, _, _) when i > 1 && i <= List.length classes && is_eliminator premises -> true
       | _ ->
          let _, conclusion = List.hd premises in
          is_appl true conclusion