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, 1 insertions, 1 deletions

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