Replace invalid tag @raises in ocamldoc comments with @raise

7 files changed, 8 insertions, 8 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
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 55b8e3a83..10fdf07e7 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -320,8 +320,8 @@ exception UniversesDiffer
 
 val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map
 (** Add the given universe unification constraints to the evar map.
-    @raises UniversesDiffer in case a first-order unification fails.
-    @raises UniverseInconsistency
+    @raise UniversesDiffer in case a first-order unification fails.
+    @raise UniverseInconsistency
 *)
 
 (** {5 Extra data}
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c5a8c7b23..11faef02c 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -798,7 +798,7 @@ let drop_parameters depth n argstk =
     s.
     @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive
     of the constructor term [c]
-    @raises Not_found if the inductive is not a primitive record, or if the
+    @raise Not_found if the inductive is not a primitive record, or if the
     constructor is partially applied.
  *)
 let eta_expand_ind_stack env ind m s (f, s') =
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 71453a04b..b9c71d72a 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -216,7 +216,7 @@ val whd_stack :
     s.
     @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive
     of the constructor term [c]
-    @raises Not_found if the inductive is not a primitive record, or if the
+    @raise Not_found if the inductive is not a primitive record, or if the
     constructor is partially applied.
  *)
 val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 51388b8f3..ce2bf85c3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -201,7 +201,7 @@ val lookup_modtype : ModPath.t -> env -> module_type_body
 (** {5 Universe constraints } *)
 
 (** Add universe constraints to the environment.
-    @raises UniverseInconsistency
+    @raise UniverseInconsistency
 *)
 val add_constraints : Univ.Constraint.t -> env -> env
 
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 97745771e..d4fba63fb 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -43,7 +43,7 @@ val check_constraint  : t -> univ_constraint -> bool
 val check_constraints : Constraint.t -> t -> bool
 
 (** 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
 
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 ->