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 /pretyping | |
| parent | 597e5dd737dd235222798153b2342ae609519348 (diff) | |
CLEANUP: in the Reduction module
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5a93230f..03e7f2642 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1264,8 +1264,8 @@ let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma -let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma +let is_trans_conv reds env sigma = test_trans_conversion Reduction.conv_universes reds env sigma +let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.conv_leq_universes reds env sigma let is_trans_fconv = function Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq let is_conv = is_trans_conv full_transparent_state @@ -1274,8 +1274,8 @@ let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with - | Reduction.CONV -> Reduction.trans_conv_universes - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CONV -> Reduction.conv_universes + | Reduction.CUMUL -> Reduction.conv_leq_universes in try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true with Reduction.NotConvertible -> false |