From 1f0d1f04b704e3368a12613f31061a53a2e40d01 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 11:06:48 +0000
Subject: Replace invalid tag @raises in ocamldoc comments with @raise

---
 kernel/cClosure.ml  | 2 +-
 kernel/cClosure.mli | 2 +-
 kernel/environ.mli  | 2 +-
 kernel/uGraph.mli   | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c5a8c7b233..11faef02cb 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 71453a04bd..b9c71d72af 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 51388b8f3b..ce2bf85c3d 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 97745771e1..d4fba63fb3 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
 
-- 
cgit v1.2.3


From efd1dd57409f5b22243c443dcde959692aabd6bd Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 14:46:12 +0000
Subject: Add empty description for @raise statements to satisfy ocamldoc

---
 kernel/environ.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index ce2bf85c3d..4e6ac1e725 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.
-    @raise UniverseInconsistency
+    @raise UniverseInconsistency .
 *)
 val add_constraints : Univ.Constraint.t -> env -> env
 
-- 
cgit v1.2.3