Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

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