diff options
| author |  mrmr1993 <mr_1993@hotmail.co.uk> | 2018-03-03 11:06:48 +0000 |
|---|---|---|
| committer | mrmr1993 <mr_1993@hotmail.co.uk> | 2018-03-05 14:35:30 +0000 |
| commit | 1f0d1f04b704e3368a12613f31061a53a2e40d01 (patch) | |
| tree | 2dd28a7d2bfa1e5a5fc8e50f293b8371db67edc8 /pretyping/reductionops.mli | |
| parent | c84509113e08372e9aa30eae57ce98f56ca95bde (diff) | |
Replace invalid tag @raises in ocamldoc comments with @raise
Diffstat (limited to 'pretyping/reductionops.mli')
| -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 16d75685d..3b56513f5 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -278,7 +278,7 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. - @raises UniverseInconsistency iff catch_incon is set to false, + @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> |