diff options
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 |