diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-09-01 16:14:03 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:39:18 +0200 |
| commit | cea3d7c83bf3aae18262e62b897ec204c098e444 (patch) | |
| tree | 9ff31a628af00e19de1b8403ef94969a675e4e9d /tactics/elimschemes.ml | |
| parent | d0b1ac17610bec74abaf122628b74c62643655d8 (diff) | |
Remove unused env argument to fresh_sort_in_family
(Universes and Evd)
Diffstat (limited to 'tactics/elimschemes.ml')
| -rw-r--r-- | tactics/elimschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 70f73df5c..3b69d9922 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -44,7 +44,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams_rec else mib.mind_nparams in - let sigma, sort = Evd.fresh_sort_in_family env sigma sort in + let sigma, sort = Evd.fresh_sort_in_family sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff |