diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 2 |
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 |