diff options
| author | coqbot-app[bot] | 2020-09-04 09:59:36 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-04 09:59:36 +0000 |
| commit | d6e8e8cba62cdfa46b1e4dfbfd6fed55b2d72df5 (patch) | |
| tree | c7d3ba4a23d427f6897afb56386d8de0213fa9b9 /vernac/comInductive.mli | |
| parent | 2000ba38718e72133b258b378b118a495acb6ffc (diff) | |
| parent | bacbd175ee22a81f170cc08959d1841847505c6d (diff) | |
Merge PR #12893: Fix incorrect debruijn handling when Record calls maybe_unify_params_in
Reviewed-by: maximedenes
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 9c876787a3..91e8f609d5 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -81,8 +81,8 @@ val template_polymorphism_candidate monomorphic universe context that can be made parametric in its conclusion sort, if one is given. *) -val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int +val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int -> EConstr.t -> Evd.evar_map (** [nparams] is the number of parameters which aren't treated as uniform, ie the length of params (including letins) where the env - is [uniform params, inductives, params]. *) + is [uniform params, inductives, params, binders]. *) |