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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 67b6839b6e..3234d40f73 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -598,12 +598,12 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
         let sigma = Proofview.Goal.sigma g in
         (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
         match EConstr.kind sigma dyn_infos.info with
-        | Case (ci, ct, iv, t, cb) ->
+        | Case (ci, u, pms, ct, iv, t, cb) ->
           let do_finalize_t dyn_info' =
             Proofview.Goal.enter (fun g ->
                 let t = dyn_info'.info in
                 let dyn_infos =
-                  {dyn_info' with info = mkCase (ci, ct, iv, t, cb)}
+                  {dyn_info' with info = mkCase (ci, u, pms, ct, iv, t, cb)}
                 in
                 let g_nb_prod =
                   nb_prod (Proofview.Goal.sigma g) (Proofview.Goal.concl g)