aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 11:06:48 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:35:30 +0000
commit1f0d1f04b704e3368a12613f31061a53a2e40d01 (patch)
tree2dd28a7d2bfa1e5a5fc8e50f293b8371db67edc8 /checker
parentc84509113e08372e9aa30eae57ce98f56ca95bde (diff)
Replace invalid tag @raises in ocamldoc comments with @raise
Diffstat (limited to 'checker')
-rw-r--r--checker/univ.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/univ.mli b/checker/univ.mli
index 3876e7bbc..935f0a2b8 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -84,7 +84,7 @@ val check_eq : universe check_function
val initial_universes : universes
(** Adds a universe to the graph, ensuring it is >= or > Set.
- @raises AlreadyDeclared if the level is already declared in the graph. *)
+ @raise AlreadyDeclared if the level is already declared in the graph. *)
exception AlreadyDeclared