aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
diff options
context:
space:
mode:
authorGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-03 14:46:12 +0000
committerGravatar mrmr1993 <mr_1993@hotmail.co.uk>2018-03-05 14:46:31 +0000
commitefd1dd57409f5b22243c443dcde959692aabd6bd (patch)
tree97998664b7a20df940a6bf06306e17d0bbf582ce /engine/evd.mli
parent7e63eb86c0435ecb67c85a332616de5cd38d0f15 (diff)
Add empty description for @raise statements to satisfy ocamldoc
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 10fdf07e7..ed3316c16 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -321,7 +321,7 @@ exception UniversesDiffer
val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map
(** Add the given universe unification constraints to the evar map.
@raise UniversesDiffer in case a first-order unification fails.
- @raise UniverseInconsistency
+ @raise UniverseInconsistency .
*)
(** {5 Extra data}