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.

5 files changed, 16 insertions, 13 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 792f07bb89..9c5f111e28 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -176,7 +176,10 @@ let fold_with_full_binders g f n acc c =
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (_,c) -> f n acc c
   | Evar (_,l) -> List.fold_left (f n) acc l
-  | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+  | Case (ci, u, pms, p, iv, c, bl) ->
+    let mib = lookup_mind (fst ci.ci_ind) in
+    let (ci, p, iv, c, bl) = Inductive.expand_case_specif mib (ci, u, pms, p, iv, c, bl) in
+    Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->
       let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -201,12 +204,11 @@ let rec traverse current ctx accu t =
 | Construct (((mind, _), _) as cst, _) ->
   traverse_inductive accu mind (ConstructRef cst)
 | Meta _ | Evar _ -> assert false
-| Case (_,oty,_,c,[||]) ->
+| Case (_, _, _, ([|_|], oty), _, c, [||]) when Vars.noccurn 1 oty ->
     (* non dependent match on an inductive with no constructors *)
-    begin match Constr.(kind oty, kind c) with
-    | Lambda(_,_,oty), Const (kn, _)
-      when Vars.noccurn 1 oty &&
-      not (Declareops.constant_has_body (lookup_constant kn)) ->
+    begin match Constr.kind c with
+    | Const (kn, _)
+      when not (Declareops.constant_has_body (lookup_constant kn)) ->
         let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
         traverse_object
           ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f715459616..cc59a96834 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -351,13 +351,13 @@ let build_beq_scheme mode kn =
             done;
 
           ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
-                        (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert,
-                                  mkVar (Id.of_string "Y") ,ar2))
+                        (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args,
+                                  NoInvert, mkVar (Id.of_string "Y") ,ar2))))
                          (constrsi.(i).cs_args))
         done;
         mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
           mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))
+            mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
     in (* build_beq_scheme *)
     let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c54adb45f9..b3ffb864f2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -69,9 +69,10 @@ let protect_pattern_in_binder bl c ctypopt =
         | LetIn (x,b,t,c) ->
           let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
           evd, mkLetIn (x,t,b,c)
-        | Case (ci,p,iv,a,bl) ->
+        | Case (ci,u,pms,p,iv,a,bl) ->
+          let (ci, p, iv, a, bl) = EConstr.expand_case env evd (ci, u, pms, p, iv, a, bl) in
           let evd,bl = Array.fold_left_map (aux env) evd bl in
-          evd, mkCase (ci,p,iv,a,bl)
+          evd, mkCase (EConstr.contract_case env evd (ci, p, iv, a, bl))
         | Cast (c,_,_)    -> f env evd c  (* we remove the cast we had set *)
         (* This last case may happen when reaching the proof of an
            impossible case, as when pattern-matching on a vector of length 1 *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2be6097184..a91771f22d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -492,7 +492,7 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
           end)
         sigma args
     | _ -> Termops.fold_constr_with_full_binders
-             sigma
+             env sigma
              (fun d (env,k) -> EConstr.push_rel d env, k+1)
              aux envk sigma c
   in
diff --git a/vernac/record.ml b/vernac/record.ml
index 68219603b4..96e4a47d2d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,7 +366,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
         let ci = Inductiveops.make_case_info env indsp rci LetStyle in
         (* Record projections are always NoInvert because they're at
            constant relevance *)
-        mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
+        mkCase (Inductive.contract_case env (ci, p, NoInvert, mkRel 1, [|branch|])), None
   in
   let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
   let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in