diff options
| author | Gaëtan Gilbert | 2019-10-09 15:16:36 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-09 15:16:36 +0200 |
| commit | b9ccd6f93ff1a0a0cf9f53030af66dd761a1315a (patch) | |
| tree | 4f9f81bc3a9041f0f55e7fe7e21305edc468edec /tactics | |
| parent | ba86025e97d3ee110978592239131865f4187b1c (diff) | |
Specialize UState.merge for extend:false
It's only called with extend:false from inside UState so we don't need
to expose it.
Not having to look at the whole `merge` function will hopefully help
those trying to understand side effects.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index f7634ba745..413c6540a3 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -140,7 +140,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) else body in - let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = |