diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-14 12:52:49 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-17 13:56:14 +0100 |
| commit | 672f8ee0c96584735294641bb4b8760e25197b80 (patch) | |
| tree | a194f3161e8de2f03482c9edc4b9d8e70ca39e27 /engine | |
| parent | 57a90691e4a64853113ab38487a5406a32c8c117 (diff) | |
CLEANUP: in the Reduction module
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 206014164..6651ff5f6 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -926,12 +926,12 @@ let update_sigma_env evd env = let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> - Reduction.conv_universes - full_transparent_state ~evars:(existential_opt_value evd) env - (UState.ugraph evd.universes) t u - | Reduction.CUMUL -> Reduction.conv_leq_universes - full_transparent_state ~evars:(existential_opt_value evd) env - (UState.ugraph evd.universes) t u + Reduction.conv env + ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) + t u + | Reduction.CUMUL -> Reduction.conv_leq env + ~evars:((existential_opt_value evd), (UState.ugraph evd.universes)) + t u let test_conversion env d pb t u = try test_conversion_gen env d pb t u; true |