diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-09 12:30:32 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-17 13:56:14 +0100 |
| commit | 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c (patch) | |
| tree | b0fb3df8a01b481283ccaa08092a351b70ac2191 /engine | |
| parent | 597e5dd737dd235222798153b2342ae609519348 (diff) | |
CLEANUP: in the Reduction module
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 425b67e08..206014164 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -926,10 +926,10 @@ let update_sigma_env evd env = let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> - Reduction.trans_conv_universes + Reduction.conv_universes full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CUMUL -> Reduction.conv_leq_universes full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u |