Merge PR #6905: Fix make ml-doc

6 files changed, 14 insertions, 14 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5163ec7b3..007d139a3 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 70f73c1fe..2bed8b624 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 21ad6e6ce..cdf1c6f95 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 f37452613..e3941c1c5 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 1f1a63dac..62c35d6df 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;
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index cd5676f28..07d0f9757 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