diff options
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index a2b7e6f3fd..ed635c0640 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -261,7 +261,7 @@ val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr -> 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 -(** [check_conv} Checks universe constraints only. +(** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool |