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.

3 files changed, 11 insertions, 9 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)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index c344fdd611..cbdebb7bbc 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -972,7 +972,7 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
                     ( UnivGen.constr_of_monomorphic_global
                     @@ Coqlib.lib_ref "core.False.type" )) ->
           tauto
-        | Case (_, _, _, v, _) ->
+        | Case (_, _, _, _, _, v, _) ->
           tclTHENLIST [simplest_case v; intros_with_rewrite ()]
         | LetIn _ ->
           tclTHENLIST
@@ -1005,7 +1005,7 @@ let rec reflexivity_with_destruct_cases () =
               (snd (destApp (Proofview.Goal.sigma g) (Proofview.Goal.concl g))).(
               2)
           with
-          | Case (_, _, _, v, _) ->
+          | Case (_, _, _, _, _, v, _) ->
             tclTHENLIST
               [ simplest_case v
               ; intros
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9d896e9182..9e9444951f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -301,10 +301,11 @@ let check_not_nested env sigma forbidden e =
     | Const _ -> ()
     | Ind _ -> ()
     | Construct _ -> ()
-    | Case (_, t, _, e, a) ->
+    | Case (_, _, pms, (_, t), _, e, a) ->
+      Array.iter check_not_nested pms;
       check_not_nested t;
       check_not_nested e;
-      Array.iter check_not_nested a
+      Array.iter (fun (_, c) -> check_not_nested c) a
     | Fix _ -> user_err Pp.(str "check_not_nested : Fix")
     | CoFix _ -> user_err Pp.(str "check_not_nested : Fix")
   in
@@ -367,7 +368,7 @@ type journey_info =
           -> unit Proofview.tactic)
       -> ( case_info
            * constr
-           * (constr, EInstance.t) case_invert
+           * case_invert
            * constr
            * constr array
          , constr )
@@ -472,7 +473,8 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) =
             ++ Printer.pr_leconstr_env env sigma expr_info.info
             ++ str " can not contain a recursive call to "
             ++ Id.print expr_info.f_id ) )
-      | Case (ci, t, iv, a, l) ->
+      | Case (ci, u, pms, t, iv, a, l) ->
+        let (ci, t, iv, a, l) = EConstr.expand_case env sigma (ci, u, pms, t, iv, a, l) in
         let continuation_tac_a =
           jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
         in
@@ -776,7 +778,7 @@ let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
       let a' = infos.info in
       let new_info =
         { infos with
-          info = mkCase (ci, a, iv, a', l)
+          info = mkCase (EConstr.contract_case env sigma (ci, a, iv, a', l))
         ; is_main_branch = expr_info.is_main_branch
         ; is_final = expr_info.is_final }
       in