Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index ac2058ba1b..343fb0b1fe 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -112,13 +112,13 @@ module Bool = struct
       else if head === negb && Array.length args = 1 then
         Negb (aux args.(0))
       else Var (Env.add env c)
-    | Case (info, r, _iv, arg, pats) ->
+    | Case (info, _, _, _, _, arg, pats) ->
       let is_bool =
         let i = info.ci_ind in
         Names.Ind.CanOrd.equal i (Lazy.force ind)
       in
       if is_bool then
-        Ifb ((aux arg), (aux pats.(0)), (aux pats.(1)))
+        Ifb ((aux arg), (aux (snd pats.(0))), (aux (snd pats.(1))))
       else
         Var (Env.add env c)
     | _ ->