diff options
| author | Hugo Herbelin | 2020-08-13 16:54:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-13 16:54:17 +0200 |
| commit | ae5f5ba7f7e673dfeb06a9feaa4271fc165d01f3 (patch) | |
| tree | 9ef80c3a604814bb9f843f916b31b8e1220f9ecb /engine/evd.ml | |
| parent | 2dbeadd72658eaa09cc9a683656aa27a4f140d50 (diff) | |
| parent | 404314c00175fcd67468bc0875c697d1c88d4650 (diff) | |
Merge PR #12720: Factor code related to class hint clenv
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index c570f75c6b..e85cbc96b2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -987,11 +987,6 @@ let check_constraints evd csts = let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } -let refresh_undefined_universes evd = - let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in - let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in - evd', subst - let nf_univ_variables evd = let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in |