diff options
| author | Matej Kosik | 2015-12-09 15:22:08 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-17 13:56:14 +0100 |
| commit | 57a90691e4a64853113ab38487a5406a32c8c117 (patch) | |
| tree | 6c12426cd43752bc4b8b1e950ba68903f4df6f7a | |
| parent | 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c (diff) | |
CLEANUP: in the Reductionops module
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 12 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 10 |
3 files changed, 9 insertions, 15 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 60d92f4beb..955bfa1656 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1099,7 +1099,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in + let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 03e7f26420..97f35fbd39 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1264,13 +1264,11 @@ 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.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 -let is_conv_leq = is_trans_conv_leq full_transparent_state -let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv_leq +let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_universes reds env sigma +let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq_universes reds env sigma +let is_fconv ?(reds=full_transparent_state) = 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 f = match pb with diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d5a844847c..43c98bbd47 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -251,13 +251,9 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : env -> evar_map -> constr -> constr -> bool -val is_conv_leq : env -> evar_map -> constr -> constr -> bool -val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool - -val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_trans_conv_leq : transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. |