diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index ce3e91db7..40409fe7f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -940,6 +940,9 @@ let add_universe_name evd s l = let universes evd = UState.ugraph evd.universes +let update_sigma_env evd env = + { evd with universes = UState.update_sigma_env evd.universes env } + (* Conversion w.r.t. an evar map and its local universes. *) let conversion_gen env evd pb t u = |