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

diff --git a/helm/software/components/acic_procedural/proceduralMode.ml b/helm/software/components/acic_procedural/proceduralMode.ml
index d2ddc6c98..e13846fc8 100644
--- a/helm/software/components/acic_procedural/proceduralMode.ml
+++ b/helm/software/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