diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 40409fe7fd..60239ebfe2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -945,7 +945,7 @@ let update_sigma_env evd env = (* Conversion w.r.t. an evar map and its local universes. *) -let conversion_gen env evd pb t u = +let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> Reduction.trans_conv_universes @@ -955,14 +955,8 @@ let conversion_gen env evd pb t u = full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u -(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) -(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) - -let conversion env d pb t u = - conversion_gen env d pb t u; d - let test_conversion env d pb t u = - try conversion_gen env d pb t u; true + try test_conversion_gen env d pb t u; true with _ -> false exception UniversesDiffer = UState.UniversesDiffer |