diff options
| author | Hugo Herbelin | 2020-03-31 23:48:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-31 23:48:49 +0200 |
| commit | 04af77a6b138bb139751053d63651f7187ea9952 (patch) | |
| tree | eda57819139540b03cf1e6a5e15ec558954bb484 /vernac/comInductive.mli | |
| parent | e98e8a03cae984a10fddc8acbe8fd781d4608b24 (diff) | |
| parent | fafc731885f84656ec884d40b843aa62a5991025 (diff) | |
Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 2b9da1d4e5..984581152a 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -88,3 +88,9 @@ val template_polymorphism_candidate polymorphic. It should have at least one universe in its 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 + -> 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]. *) |