]> matita.cs.unibo.it Git - helm.git/blobdiff - components/acic_procedural/proceduralMode.ml
GrafiteAstPp: \n's finally fixed
[helm.git] / components / acic_procedural / proceduralMode.ml
index d2ddc6c9847c37d0c25dba76cc9a4dde0c9de096..e13846fc85a3ddee2b6dbb4f805be0ab7fac1de6 100644 (file)
@@ -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