diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/univ.mli | 2 |
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 |