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.

9 files changed, 44 insertions, 30 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)
     | _ ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6869f9c47e..0cad192332 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -672,9 +672,11 @@ let rec extract_term env sg mle mlt c args =
         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
         let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
         in extract_app env sg mle mlt extract_rel args
-    | Case ({ci_ind=ip},_,iv,c0,br) ->
-      (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
-      extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
+    | Case (ci, u, pms, r, iv, c0, br) ->
+        (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
+        let (ip, r, iv, c0, br) = EConstr.expand_case env sg (ci, u, pms, r, iv, c0, br) in
+        let ip = ci.ci_ind in
+        extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
         extract_app env sg mle mlt (extract_fix env sg mle i recd) args
     | CoFix (i,recd) ->
@@ -1078,9 +1080,13 @@ let fake_match_projection env p =
         let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
         fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
       else
-        let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
-        let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
-        let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in
+        let p = ([|x|], liftn 1 2 ty) in
+        let branch =
+          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
+          (nas, mkRel (List.length ctx - (j - 1)))
+        in
+        let params = Context.Rel.to_extended_vect mkRel 1 paramslet in
+        let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
         it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
     | LocalDef (_,c,t) :: rem ->
       let c = liftn 1 j c in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index c62bc73e41..e208ba9a5c 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -67,10 +67,13 @@ let unif env evd t1 t2=
           | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
           | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
               Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
-          | Case (_,pa,_,ca,va),Case (_,pb,_,cb,vb)->
-            Queue.add (pa,pb) bige;
-            Queue.add (ca,cb) bige;
-            let l=Array.length va in
+          | Case (cia,ua,pmsa,pa,iva,ca,va),Case (cib,ub,pmsb,pb,ivb,cb,vb)->
+            let env = Global.env () in
+            let (cia,pa,iva,ca,va) = EConstr.expand_case env evd (cia,ua,pmsa,pa,iva,ca,va) in
+            let (cib,pb,iva,cb,vb) = EConstr.expand_case env evd (cib,ub,pmsb,pb,ivb,cb,vb) in
+              Queue.add (pa,pb) bige;
+              Queue.add (ca,cb) bige;
+              let l=Array.length va in
                 if not (Int.equal l (Array.length vb)) then
                   raise (UFAIL (nt1,nt2))
                 else
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
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2c298caa..90c366ed63 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -774,7 +774,7 @@ let rec find_a_destructable_match sigma t =
   let cl = [cl, (None, None), None], None in
   let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
   match EConstr.kind sigma t with
-    | Case (_,_,_,x,_) when closed0 sigma x ->
+    | Case (_,_,_,_,_,x,_) when closed0 sigma x ->
         if isVar sigma x then
           (* TODO check there is no rel n. *)
           raise (Found (Tacinterp.eval_tactic dest))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 59533eb3e3..6d0e0c36b3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -918,7 +918,8 @@ let reset_env env =
     Environ.push_rel_context (Environ.rel_context env) env'
 
 let fold_match ?(force=false) env sigma c =
-  let (ci, p, iv, c, brs) = destCase sigma c in
+  let case = destCase sigma c in
+  let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in
   let cty = Retyping.get_type_of env sigma c in
   let dep, pred, exists, sk =
     let env', ctx, body =
@@ -986,7 +987,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
                     let argty = Retyping.get_type_of env (goalevars evars) arg in
                     let state, res = s.strategy { state ; env ;
                                                   unfresh ;
-                                                  term1 = arg ;	ty1 = argty ;
+                                                  term1 = arg ;        ty1 = argty ;
                                                   cstr = (prop,None) ;
                                                   evars } in
                     let res' =
@@ -1153,7 +1154,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
           | Fail | Identity -> b'
         in state, res
 
-      | Case (ci, p, iv, c, brs) ->
+      | Case (ci, u, pms, p, iv, c, brs) ->
+        let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
         let cty = Retyping.get_type_of env (goalevars evars) c in
         let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
         let cstr' = Some eqty in
@@ -1163,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
         let state, res =
           match c' with
           | Success r ->
-            let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
+            let case = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in
             let res = make_leibniz_proof env case ty r in
               state, Success (coerce env (prop,cstr) res)
           | Fail | Identity ->
@@ -1185,7 +1187,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
               in
                 match found with
                 | Some r ->
-                  let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+                  let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
                     state, Success (make_leibniz_proof env ctxc ty r)
                 | None -> state, c'
             else
@@ -1386,7 +1388,7 @@ module Strategies =
 
     let fold_glob c : 'a pure_strategy = { strategy =
       fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
-(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
+(*         let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
         let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
         let unfolded =
           try Tacred.try_red_product env sigma c
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 2a21049c6e..7774258fca 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -285,7 +285,8 @@ let iter_constr_LR f c = match kind c with
   | Prod (_, t, b) | Lambda (_, t, b)  -> f t; f b
   | LetIn (_, v, t, b) -> f v; f t; f b
   | App (cf, a) -> f cf; Array.iter f a
-  | Case (_, p, iv, v, b) -> f v; iter_invert f iv; f p; Array.iter f b
+  | Case (_, _, pms, (_, p), iv, v, b) ->
+    f v; Array.iter f pms; f p; iter_invert f iv; Array.iter (fun (_, c) -> f c) b
   | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) ->
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
   | Proj(_,a) -> f a
@@ -749,7 +750,7 @@ let rec uniquize = function
         EConstr.push_rel ctx_item env, h' + 1 in
       let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in
       let f = EConstr.of_constr f in
-      let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in
+      let f' = map_constr_with_binders_left_to_right env sigma inc_h self acc f in
       let f' = EConstr.Unsafe.to_constr f' in
       mkApp (f', Array.map_left (subst_loop acc) a) in
   subst_loop (env,h) c) : find_P),