diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-09 15:22:08 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-17 13:56:14 +0100 |
| commit | 57a90691e4a64853113ab38487a5406a32c8c117 (patch) | |
| tree | 6c12426cd43752bc4b8b1e950ba68903f4df6f7a /pretyping/reductionops.mli | |
| parent | 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c (diff) | |
CLEANUP: in the Reductionops module
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d5a844847..43c98bbd4 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. |