From ceb190dc44ab1b251e799546c0a7ec298fd2f72e Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 11:02:59 +0000
Subject: Tweak comments to fix ocamldoc errors

---
 engine/proofview.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 25c8e2d802..8a844bbf54 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -127,7 +127,7 @@ let focus_context (left,right) =
 
 (** This (internal) function extracts a sublist between two indices,
     and returns this sublist together with its context: if it returns
-    [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the
+    [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the
     original list.  The focused list has lenght [j-i-1] and contains
     the goals from number [i] to number [j] (both included) the first
     goal of the list being numbered [1].  [focus_sublist i j l] raises
@@ -572,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
 
 
 (** [extend_to_list startxs rx endxs l] builds a list
-    [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises
-    [SizeMismatch] if [startxs@endxs] is already longer than [l]. *)
+    [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises
+    [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *)
 let extend_to_list startxs rx endxs l =
   (* spiwack: I use [l] essentially as a natural number *)
   let rec duplicate acc = function
-- 
cgit v1.2.3


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

---
 engine/evd.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.mli b/engine/evd.mli
index 55b8e3a832..10fdf07e72 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}
-- 
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

---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/evd.mli b/engine/evd.mli
index 10fdf07e72..ed3316c16d 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}
-- 
cgit v1.2.3