diff options
| author | Pierre-Marie Pédrot | 2018-06-22 00:43:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:29:55 +0100 |
| commit | 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 (patch) | |
| tree | 9f54ad363b2c8f855be97860ba1900572353e164 /pretyping/reductionops.ml | |
| parent | ecfbeaa62f9d8bd4dc4600cf39df2262af718313 (diff) | |
Move transparent_state to its own module.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 17003cd1dd..18b0bab892 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1305,13 +1305,13 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma -let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma -let is_fconv ?(reds=full_transparent_state) = function +let is_conv ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv reds env sigma +let is_conv_leq ?(reds=TranspState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma +let is_fconv ?(reds=TranspState.full) = function | Reduction.CONV -> is_conv ~reds | Reduction.CUMUL -> is_conv_leq ~reds -let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = +let check_conv ?(pb=Reduction.CUMUL) ?(ts=TranspState.full) env sigma x y = let f = match pb with | Reduction.CONV -> f_conv | Reduction.CUMUL -> f_conv_leq @@ -1345,7 +1345,7 @@ let sigma_univ_state = compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) - ?(ts=full_transparent_state) env sigma x y = + ?(ts=TranspState.full) env sigma x y = (** FIXME *) try let ans = match pb with @@ -1378,7 +1378,7 @@ let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) (* This reference avoids always having to link C code with the kernel *) -let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state) +let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TranspState.full) let set_vm_infer_conv f = vm_infer_conv := f let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = !vm_infer_conv ~pb env t1 t2 |