From 90dcc8ff89a495d18d319ecb6036f777e697089d Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 10:56:12 +0000
Subject: Use computed deps to generate ml-doc and use implicit mli-doc deps

---
 Makefile.doc | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Makefile.doc b/Makefile.doc
index 894ef9a99a..746ed14696 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -387,10 +387,9 @@ install-doc-index-urls:
 
 OCAMLDOCDIR=dev/ocamldoc
 
-DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
-	./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
-	./parsing/*.mli ./proofs/*.mli \
-	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
+DOCMLS=$(foreach lib,$(CORECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .ml, $($(lib))))
+
+DOCMLIS=$(wildcard $(addsuffix /*.mli, $(CORESRCDIRS)))
 
 # Defining options to generate dependencies graphs
 DOT=dot
@@ -434,7 +433,7 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
 	$(OCAMLDOC_MLLIBD)
 
 ml-doc:
-	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
+	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(DOCMLS)
 
 parsing/parsing.dot : | parsing/parsing.mllib.d
 	$(OCAMLDOC_MLLIBD)
-- 
cgit v1.2.3


From 9d44eb55a515511e6d9bb2fa093b34a987753335 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 11:00:50 +0000
Subject: Tidy up ml-doc outut, give it a separate output directory

---
 Makefile.doc | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Makefile.doc b/Makefile.doc
index 746ed14696..9325ef7e60 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -433,7 +433,12 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -
 	$(OCAMLDOC_MLLIBD)
 
 ml-doc:
-	$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(DOCMLS)
+	$(SHOW)'OCAMLDOC -html'
+	$(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation
+	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \
+	$(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \
+	-t "Coq mls documentation" \
+	-css-style ../style.css
 
 parsing/parsing.dot : | parsing/parsing.mllib.d
 	$(OCAMLDOC_MLLIBD)
-- 
cgit v1.2.3


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

---
 clib/option.ml       | 2 +-
 engine/proofview.ml  | 6 +++---
 tactics/hipattern.ml | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/clib/option.ml b/clib/option.ml
index c2e2e70970..21913e8f7a 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -44,7 +44,7 @@ let hash f = function
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y].
-    @raise [IsNone] if [x] equals [None]. *)
+    @raise IsNone if [x] equals [None]. *)
 let get = function
   | Some y -> y
   | _ -> raise IsNone
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
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a59046a678..b012a7ecd1 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -511,10 +511,10 @@ let coq_eqdec ~sum ~rev =
     mkPattern (mkGAppRef sum args)
   )
 
-(** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *)
+(** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *)
 let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false
 
-(** { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } *)
+(** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *)
 let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true
 
 (** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *)
-- 
cgit v1.2.3


From c84509113e08372e9aa30eae57ce98f56ca95bde Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 11:03:35 +0000
Subject: Remove non-existent dependency

---
 lib/lib.mllib | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lib/lib.mllib b/lib/lib.mllib
index b2260ba097..0891859423 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -15,7 +15,6 @@ CWarnings
 Rtree
 System
 Explore
-RTree
 CProfile
 Future
 Spawn
-- 
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

---
 checker/univ.mli           | 2 +-
 engine/evd.mli             | 4 ++--
 kernel/cClosure.ml         | 2 +-
 kernel/cClosure.mli        | 2 +-
 kernel/environ.mli         | 2 +-
 kernel/uGraph.mli          | 2 +-
 pretyping/reductionops.mli | 2 +-
 7 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/checker/univ.mli b/checker/univ.mli
index 3876e7bbc9..935f0a2b8d 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 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}
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
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 16d75685d4..3b56513f5e 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 -> 
-- 
cgit v1.2.3


From fb4571bf487fd590d5e64ee33b27a7212a491466 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 11:11:15 +0000
Subject: Fix formatting of some ocamldoc comments to reduce warnings

---
 interp/constrintern.ml | 2 +-
 intf/constrexpr.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 84162ca89b..918e12e5cb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1077,7 +1077,7 @@ type 'a raw_cases_pattern_expr_r =
   | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
   | RCPatCstr  of Globnames.global_reference
     * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
-  (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
+  (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
   | RCPatAtom  of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
   | RCPatOr    of 'a raw_cases_pattern_expr list
 and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 474b80ec48..0d5542277f 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -51,7 +51,7 @@ type cases_pattern_expr_r =
   | CPatAlias of cases_pattern_expr * lname
   | CPatCstr  of reference
     * cases_pattern_expr list option * cases_pattern_expr list
-  (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
+  (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
   | CPatAtom of reference option
   | CPatOr   of cases_pattern_expr list
   | CPatNotation of notation * cases_pattern_notation_substitution
-- 
cgit v1.2.3


From 4d916a65ef1274160a2ee9726b88de5245e800e8 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 11:25:26 +0000
Subject: Change non-documentation comment from ocamldoc style

---
 intf/constrexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 0d5542277f..647c01ff52 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -121,7 +121,7 @@ and recursion_order_expr =
   | CWfRec of constr_expr
   | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
 
-(** Anonymous defs allowed ?? *)
+(* Anonymous defs allowed ?? *)
 and local_binder_expr =
   | CLocalAssum   of lname list * binder_kind * constr_expr
   | CLocalDef     of lname * constr_expr * constr_expr option
-- 
cgit v1.2.3


From 5fda90cfe7ad79ee4e32681643b40d9fd0e573ee Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 14:03:24 +0000
Subject: Build docs for plugins by default, add NOPLUGINDOCS flag to disable

---
 Makefile.doc | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/Makefile.doc b/Makefile.doc
index 9325ef7e60..8c34c94725 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -385,11 +385,18 @@ install-doc-index-urls:
 # Documentation of the source code (using ocamldoc)
 ###########################################################################
 
+# To skip building docs for plugins and build docs for core only, set this
+# variable to 1 (or any non-empty value):
+NOPLUGINDOCS ?=
+
 OCAMLDOCDIR=dev/ocamldoc
 
-DOCMLS=$(foreach lib,$(CORECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .ml, $($(lib))))
+DOCMLLIBS=$(if $(NOPLUGINDOCS), \
+		  $(CORECMA:.cma=_MLLIB_DEPENDENCIES), \
+		  $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES))
+DOCMLS=$(foreach lib,$(DOCMLLIBS),$(addsuffix .ml, $($(lib))))
 
-DOCMLIS=$(wildcard $(addsuffix /*.mli, $(CORESRCDIRS)))
+DOCMLIS=$(wildcard $(addsuffix /*.mli, $(if $(NOPLUGINDOCS),$(CORESRCDIRS),$(SRCDIRS))))
 
 # Defining options to generate dependencies graphs
 DOT=dot
-- 
cgit v1.2.3


From b88790fc8d473af4afd8dd59af61c137068e0376 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 14:38:43 +0000
Subject: Separate vim/emacs fold markers from ocamldoc comments

ocamldoc chokes on the markers {{{ and }}} because { and } are part of
its syntax
---
 plugins/ssr/ssrcommon.ml            | 8 ++++----
 plugins/ssr/ssrparser.ml4           | 6 +++---
 plugins/ssr/ssrtacticals.ml         | 2 +-
 plugins/ssr/ssrvernac.ml4           | 6 +++---
 plugins/ssrmatching/ssrmatching.ml4 | 4 ++--
 5 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5163ec7b36..007d139a33 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -460,7 +460,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with
 
 let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac
 
-(** Open term to lambda-term coercion  {{{ ************************************)
+(** Open term to lambda-term coercion  *)(* {{{ ************************************)
 
 (* This operation takes a goal gl and an open term (sigma, t), and   *)
 (* returns a term t' where all the new evars in sigma are abstracted *)
@@ -1000,7 +1000,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
   try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
-(** Profiling {{{ *************************************************************)
+(** Profiling *)(* {{{ *************************************************************)
 type profiler = { 
   profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
   reset : unit -> unit;
@@ -1128,7 +1128,7 @@ let interp_clr sigma = function
 
 (** Basic tacticals *)
 
-(** Multipliers {{{ ***********************************************************)
+(** Multipliers *)(* {{{ ***********************************************************)
 
 (* tactical *)
 
@@ -1168,7 +1168,7 @@ let tclMULT = function
 let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr))
 let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr)
 
-(** }}} *)
+(* }}} *)
 
 (** Generalize tactic *)
 
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 70f73c1fe7..2bed8b624b 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint
 ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint
 | [ ]                       -> [ nohint ]
 END
-(** The "in" pseudo-tactical {{{ **********************************************)
+(** The "in" pseudo-tactical *)(* {{{ **********************************************)
 
 (* We can't make "in" into a general tactical because this would create a  *)
 (* crippling conflict with the ltac let .. in construct. Hence, we add     *)
@@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr
 let old_tac = V82.tactic
 
 
-(** Name generation {{{ *******************************************************)
+(** Name generation *)(* {{{ *******************************************************)
 
 (* Since Coq now does repeated internal checks of its external lexical *)
 (* rules, we now need to carve ssreflect reserved identifiers out of   *)
@@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag)
 
 (* We must not anonymize context names discharged by the "in" tactical. *)
 
-(** Tactical extensions. {{{ **************************************************)
+(** Tactical extensions. *)(* {{{ **************************************************)
 
 (* The TACTIC EXTEND facility can't be used for defining new user   *)
 (* tacticals, because:                                              *)
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 21ad6e6ced..cdf1c6f953 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -59,7 +59,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) =
   | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3
   | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad))
 
-(** The "in" pseudo-tactical {{{ **********************************************)
+(** The "in" pseudo-tactical *)(* {{{ **********************************************)
 
 let hidden_goal_tag = "the_hidden_goal"
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index f374526131..e3941c1c5d 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
 
 (* global syntactic changes and vernacular commands *)
 
-(** Alternative notations for "match" and anonymous arguments. {{{ ************)
+(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************)
 
 (* Syntax:                                                        *)
 (*  if <term> is <pattern> then ... else ...                      *)
@@ -127,7 +127,7 @@ GEXTEND Gram
 END
 (* }}} *)
 
-(** Vernacular commands: Prenex Implicits and Search {{{ **********************)
+(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************)
 
 (* This should really be implemented as an extension to the implicit   *)
 (* arguments feature, but unfortuately that API is sealed. The current *)
@@ -461,7 +461,7 @@ END
 
 (* }}} *)
 
-(** View hint database and View application. {{{ ******************************)
+(** View hint database and View application. *)(* {{{ ******************************)
 
 (* There are three databases of lemmas used to mediate the application  *)
 (* of reflection lemmas: one for forward chaining, one for backward     *)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 1f1a63daca..62c35d6dfa 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -70,7 +70,7 @@ let _ =
       Goptions.optwrite = debug }
 let pp s = !pp_ref s
 
-(** Utils {{{ *****************************************************************)
+(** Utils *)(* {{{ *****************************************************************)
 let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind c with App (f, a) -> f, a | _ -> c, [| |]
@@ -179,7 +179,7 @@ let nf_evar sigma c =
 
 (* }}} *)
 
-(** Profiling {{{ *************************************************************)
+(** Profiling *)(* {{{ *************************************************************)
 type profiler = { 
   profile : 'a 'b. ('a -> 'b) -> 'a -> 'b;
   reset : unit -> unit;
-- 
cgit v1.2.3


From 7e63eb86c0435ecb67c85a332616de5cd38d0f15 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 14:44:27 +0000
Subject: Escape curly braces in ocamldoc comment

---
 plugins/ssrmatching/ssrmatching.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index cd5676f28c..07d0f97575 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -74,7 +74,7 @@ val interp_cpattern :
     pattern
 
 (** The set of occurrences to be matched. The boolean is set to true
- *  to signal the complement of this set (i.e. {-1 3}) *)
+ *  to signal the complement of this set (i.e. \{-1 3\}) *)
 type occ = (bool * int list) option
 
 (** [subst e p t i]. [i] is the number of binders
-- 
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 +-
 kernel/environ.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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}
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


From 65701510e61651c91d4c256c04499cc3cf38794c Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Sat, 3 Mar 2018 15:10:49 +0000
Subject: Remove NOPLUGINDOCS option

---
 Makefile.doc | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/Makefile.doc b/Makefile.doc
index 8c34c94725..9fd93651d1 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -385,18 +385,12 @@ install-doc-index-urls:
 # Documentation of the source code (using ocamldoc)
 ###########################################################################
 
-# To skip building docs for plugins and build docs for core only, set this
-# variable to 1 (or any non-empty value):
-NOPLUGINDOCS ?=
-
 OCAMLDOCDIR=dev/ocamldoc
 
-DOCMLLIBS=$(if $(NOPLUGINDOCS), \
-		  $(CORECMA:.cma=_MLLIB_DEPENDENCIES), \
-		  $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES))
+DOCMLLIBS= $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES)
 DOCMLS=$(foreach lib,$(DOCMLLIBS),$(addsuffix .ml, $($(lib))))
 
-DOCMLIS=$(wildcard $(addsuffix /*.mli, $(if $(NOPLUGINDOCS),$(CORESRCDIRS),$(SRCDIRS))))
+DOCMLIS=$(wildcard $(addsuffix /*.mli, $(SRCDIRS)))
 
 # Defining options to generate dependencies graphs
 DOT=dot
-- 
cgit v1.2.3