diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-05 12:56:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-05 12:56:27 +0200 |
| commit | d19605b7bfb8425b53be4cab30bef462c4fa4d14 (patch) | |
| tree | 2bdcc15e217c24ca33b2fe48537c8632562a9ec1 /tactics/elimschemes.ml | |
| parent | 7413f8532879c64e05ee0e8ca16693d74fe84ab9 (diff) | |
| parent | 08b2fde7054a61e5468ef90eabb0d348730f170e (diff) | |
Merge PR #7746: Many small cleanups removing unused arguments and functions
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 |