Fixing ml-doc.

8 files changed, 49 insertions, 61 deletions

diff --git a/Makefile.build b/Makefile.build
index dd7b20f0f..db2d0f720 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -707,13 +707,13 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
 	-intro $(OCAMLDOCDIR)/docintro -o $@
 
 mli-doc: $(DOCMLIS:.mli=.cmi)
-	$(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(OCAMLDOC) -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) $(COQIDEFLAGS)\
 	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
 
 ml-dot: $(MLFILES)
-	$(OCAMLDOC) -dot -dot-reduce -rectypes -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(OCAMLDOC) -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) $(COQIDEFLAGS)\
 	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
 
 %_dep.png: %.dot
@@ -729,7 +729,7 @@ OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
 	$(OCAMLDOC_MLLIBD)
 
 ml-doc:
-	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES)
+	$(OCAMLDOC) -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES)
 
 parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
 	$(OCAMLDOC_MLLIBD)
diff --git a/ide/sentence.ml b/ide/sentence.ml
index 9c361c81f..557a86b2b 100644
--- a/ide/sentence.ml
+++ b/ide/sentence.ml
@@ -67,7 +67,7 @@ let rec grab_sentence_stop (start:GText.iter) =
   (forward_search is_sentence_end start)#forward_char
 
 (** Search forward the first character immediately after a "." sentence end
-    (and not just a "{" or "}" or comment end *)
+    (and not just a "\{" or "\}" or comment end *)
 
 let rec grab_ending_dot (start:GText.iter) =
   let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f38a2c314..1f6effba6 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -21,7 +21,7 @@ open Pre_env
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
 
-(** Local names {{{**)
+(** Local names **)
 
 type lname = { lname : name; luid : int }
 
@@ -42,9 +42,8 @@ let reset_lname = lname_ctr := -1
 let fresh_lname n = 
   incr lname_ctr;
   { lname = n; luid = !lname_ctr }
-  (**}}}**)
 
-(** Global names {{{ **)
+(** Global names **)
 type gname = 
   | Gind of string * inductive (* prefix, inductive name *)
   | Gconstruct of string * constructor (* prefix, constructor name *)
@@ -136,9 +135,8 @@ let reset_normtbl () = normtbl_ctr := -1
 let fresh_gnormtbl l =
   incr normtbl_ctr;
   Gnormtbl (l,!normtbl_ctr)
-  (**}}}**)
 
-(** Symbols (pre-computed values) {{{**)
+(** Symbols (pre-computed values) **)
 
 type symbol =
   | SymbValue of Nativevalues.t
@@ -241,9 +239,9 @@ let symbols_tbl_name = Ginternal "symbols_tbl"
 
 let get_symbols_tbl () =
   let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
-  HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl(**}}}**)
+  HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
 
-(** Lambda to Mllambda {{{**)
+(** Lambda to Mllambda **)
 
 type primitive =
   | Mk_prod
@@ -1250,9 +1248,8 @@ let mllambda_of_lambda auxdefs l t =
   (* final result : global list, fv, ml *)
   else
     (!global_stack, (fv_named, fv_rel), mkMLlam (Array.of_list params) ml)
-    (**}}}**)
 
-(** Code optimization {{{**)
+(** Code optimization **)
 
 (** Optimization of match and fix *)
 
@@ -1408,9 +1405,8 @@ let optimize_stk stk =
         Glet(Gconstant (prefix, c), optimize gdef body)
     | _ -> g in
   List.map optimize_global stk
-  (**}}}**)
 
-(** Printing to ocaml {{{**)
+(** Printing to ocaml **)
 (* Redefine a bunch of functions in module Names to generate names
    acceptable to OCaml. *)
 let string_of_id s = Unicode.ascii_of_ident (string_of_id s)
@@ -1708,9 +1704,9 @@ let pp_global fmt g =
 	pp_gname gn pp_ldecls params 
 	pp_mllam (MLmatch(annot,a,accu,bs))
   | Gcomment s ->
-      Format.fprintf fmt "@[(* %s *)@]@." s(**}}}**)
+      Format.fprintf fmt "@[(* %s *)@]@." s
 
-(** Compilation of elements in environment {{{**)
+(** Compilation of elements in environment **)
 let rec compile_with_fv env sigma auxdefs l t =
   let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
   if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
@@ -1961,6 +1957,5 @@ let update_locations (ind_updates,const_updates) =
 
 let add_header_comment mlcode s =
   Gcomment s :: mlcode
-(** }}} **)
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/lib/serialize.ml b/lib/serialize.ml
index c97817779..042b75e2d 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -19,7 +19,7 @@ open Interface
 open Xml_datatype
 
 (* Marshalling of basic types and type constructors *)
-module Xml_marshalling = struct (* {{{ *)
+module Xml_marshalling = struct
 
 exception Marshal_error
 
@@ -370,12 +370,12 @@ let to_feedback xml = match xml with
       content = to_feedback_content content }
   | _ -> raise Marshal_error
 
-end (* }}} *)
+end
 include Xml_marshalling
 
 (* Reification of basic types and type constructors, and functions
    from to xml *)
-module ReifType : sig (* {{{ *)
+module ReifType : sig
 
   type 'a val_t
 
@@ -609,7 +609,7 @@ end = struct
       (pr_xml (of_option_state { opt_sync = true; opt_depr = false;
         opt_name = "name1"; opt_value = IntValue (Some 37) }));
 
-end  (* }}} *)
+end
 open ReifType
 
 (** Types reification, checked with explicit casts *)
@@ -755,7 +755,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value =
   with any ->
     Fail (handler.handle_exn any)
 
-(** brain dead code, edit if protocol messages are added/removed {{{ *)
+(** brain dead code, edit if protocol messages are added/removed *)
 let of_answer (q : 'a call) (v : 'a value) : xml = match q with
   | Add _        -> of_value (of_value_type add_rty_t        ) (Obj.magic v)
   | Edit_at _    -> of_value (of_value_type edit_at_rty_t    ) (Obj.magic v)
@@ -833,7 +833,6 @@ let to_call : xml -> unknown call =
     | "Interp"     -> Interp     (mkCallArg interp_sty_t      a)
     | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a)
     | _ -> raise Marshal_error)
-(* }}} *)
 
 (** misc *)
 
@@ -841,7 +840,7 @@ let is_feedback = function
   | Element ("feedback", _, _) -> true
   | _ -> false
 
-(** {{{ Debug printing *)
+(** Debug printing *)
 
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
@@ -885,8 +884,6 @@ let pr_call call = match call with
   | Interp x     -> str_of_call call ^ " " ^ print interp_sty_t      x
   | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x
 
-(* }}} *)
-
 let document to_string_fmt =
   Printf.printf "=== Available calls ===\n\n";
   Array.iter (fun (cname, csty, crty) ->
diff --git a/library/declaremods.ml b/library/declaremods.ml
index bb623b7a1..e4f227637 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -332,7 +332,7 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs
 
 
 
-(** {6 From module expression to substitutive objects *)
+(** {6 From module expression to substitutive objects} *)
 
 (** Turn a chain of [MSEapply] into the head module_path and the
     list of module_path parameters (deepest param coming first).
@@ -668,7 +668,7 @@ let declare_module interp_modast id args res mexpr_o fs =
 
 end
 
-(** {6 Module types : start, end, declare *)
+(** {6 Module types : start, end, declare} *)
 
 module RawModTypeOps = struct
 
@@ -787,7 +787,7 @@ let declare_include interp me_asts =
 end
 
 
-(** {6 Module operations handling summary freeze/unfreeze *)
+(** {6 Module operations handling summary freeze/unfreeze} *)
 
 let protect_summaries f =
   let fs = Summary.freeze_summaries ~marshallable:`No in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index db998f32b..9515c5de9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -45,7 +45,7 @@ type tag = Tag.t
 
 (**
   * An atom is of the form:
-  *   pExpr1 {<,>,=,<>,<=,>=} pExpr2
+  *   pExpr1 \{<,>,=,<>,<=,>=\} pExpr2
   * where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are
   * parametrized by 'cst, which is used as the type of constants.
   *)
@@ -112,7 +112,7 @@ let rec ids_of_formula f =
 (**
   * A clause is a list of (tagged) nFormulas.
   * nFormulas are normalized formulas, i.e., of the form:
-  *   cPol {=,<>,>,>=} 0
+  *   cPol \{=,<>,>,>=\} 0
   * with cPol compact polynomials (see the Pol inductive type in EnvRing.v).
   *)
 
@@ -246,7 +246,7 @@ let rec add_term  t0 = function
 module ISet = Set.Make(Int)
 
 (**
-  * Given a set of integers s={i0,...,iN} and a list m, return the list of
+  * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
   * elements of m that are at position i0,...,iN.
   *)
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index a6c2e0a59..050bd310d 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -19,10 +19,10 @@ struct
   type interval = num option * num option
       (** None models the absence of bound i.e. infinity *)
       (** As a result,
-	  - None , None   -> ]-oo,+oo[
-	  - None , Some v -> ]-oo,v]
-	  - Some v, None  -> [v,+oo[
-	  - Some v, Some v' -> [v,v']
+	  - None , None   -> \]-oo,+oo\[
+	  - None , Some v -> \]-oo,v\]
+	  - Some v, None  -> \[v,+oo\[
+	  - Some v, Some v' -> \[v,v'\]
       Intervals needs to be explicitely normalised.
       *)
 
@@ -117,7 +117,7 @@ and cstr_info = {
 }
 
 
-(** A system of constraints has the form [{sys = s ; vars = v}].
+(** A system of constraints has the form [\{sys = s ; vars = v\}].
     [s] is a hashtable mapping a normalised vector to a [cstr_info] record where
     - [bound] is an interval
     - [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint.
@@ -499,7 +499,7 @@ let pick_small_value bnd =
 	then ceiling_num i (* why not *) else i
 
 
-(** [solution s1 sys_l  = Some(sn,[(vn-1,sn-1);...; (v1,s1)]@sys_l)]
+(** [solution s1 sys_l  = Some(sn,\[(vn-1,sn-1);...; (v1,s1)\]\@sys_l)]
     then [sn] is a  system which contains only [black_v] -- if it existed in [s1]
     and [sn+1] is obtained by projecting [vn] out of [sn]
     @raise SystemContradiction if  system [s] has no solution
diff --git a/stm/stm.ml b/stm/stm.ml
index e791e37cf..6fe3fd03a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -130,7 +130,7 @@ module Vcs_aux : sig
   exception Expired
   val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
 
-end = struct (* {{{ *)
+end = struct
 
   let proof_nesting vcs =
     List.fold_left max 0
@@ -171,7 +171,7 @@ end = struct (* {{{ *)
       | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
     with Not_found -> raise Expired
 
-end (* }}} *)
+end
 
 (* Imperative wrap around VCS to obtain _the_ VCS *)
 module VCS : sig
@@ -234,7 +234,7 @@ module VCS : sig
   val backup : unit -> vcs
   val restore : vcs -> unit
 
-end = struct (* {{{ *)
+end = struct
 
   include Vcs_
   exception Expired = Vcs_aux.Expired
@@ -242,7 +242,7 @@ end = struct (* {{{ *)
   module StateidSet = Set.Make(Stateid)
   open Printf
 
-  let print_dag vcs () = (* {{{ *)
+  let print_dag vcs () =
     let fname = "stm_" ^ process_id () in
     let string_of_transaction = function
       | Cmd (t, _) | Fork (t, _,_,_) ->
@@ -325,8 +325,7 @@ end = struct (* {{{ *)
     close_out oc;
     ignore(Sys.command
       ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
-  (* }}} *)
-  
+
   type vcs = (branch_type, transaction, vcs state_info) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
@@ -454,7 +453,7 @@ end = struct (* {{{ *)
 
     val command : now:bool -> (unit -> unit) -> unit
 
-  end = struct (* {{{ *)
+  end = struct
     
     let m = Mutex.create ()
     let c = Condition.create ()
@@ -486,7 +485,7 @@ end = struct (* {{{ *)
           worker := Some (Thread.create run_command ())
       end
 
-  end (* }}} *)
+  end
 
   let print ?(now=false) () =
     if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs)
@@ -494,7 +493,7 @@ end = struct (* {{{ *)
   let backup () = !vcs
   let restore v = vcs := v
 
-end (* }}} *)
+end
 
 (* Fills in the nodes of the VCS *)
 module State : sig
@@ -517,7 +516,7 @@ module State : sig
   val get_cached : Stateid.t -> frozen_state
   val assign : Stateid.t -> frozen_state -> unit
 
-end = struct (* {{{ *)
+end = struct
 
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
@@ -600,7 +599,6 @@ end = struct (* {{{ *)
       | None -> raise (exn_on id ~valid:good_id e)
 
 end
-(* }}} *)
 
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
@@ -670,7 +668,7 @@ module Slaves : sig
 
   val set_perspective : Stateid.t list -> unit
 
-end = struct (* {{{ *)
+end = struct
 
 
   let cancel_worker n = WorkersPool.cancel (n-1)
@@ -1152,7 +1150,7 @@ end = struct (* {{{ *)
     List.map (function ReqBuildProof(a,b,c,d,x,e) ->
       ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks
 
-end (* }}} *)
+end
 
 (* Runs all transactions needed to reach a state *)
 module Reach : sig
@@ -1160,7 +1158,7 @@ module Reach : sig
   val known_state :
     ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
 
-end = struct (* {{{ *)
+end = struct
 
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
@@ -1366,7 +1364,8 @@ let known_state ?(redefine_qed=false) ~cache id =
     prerr_endline ("reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
-end (* }}} *)
+end
+
 let _ = Slaves.set_reach_known_state Reach.known_state
 
 (* The backtrack module simulates the classic behavior of a linear document *)
@@ -1382,7 +1381,7 @@ module Backtrack : sig
   (* To be installed during initialization *)
   val undo_vernac_classifier : vernac_expr -> vernac_classification
 
-end = struct (* {{{ *)
+end = struct
 
   let record () =
     let current_branch = VCS.current_branch () in
@@ -1497,7 +1496,7 @@ end = struct (* {{{ *)
        msg_warning(str"undo_vernac_classifier: going back to the initial state.");
        VtStm (VtBack Stateid.initial, true), VtNow
 
-end (* }}} *)
+end
 
 let init () =
   VCS.init Stateid.initial;
@@ -1806,7 +1805,7 @@ let process_transaction ~tty verbose c (loc, expr) =
     let e = Errors.push e in
     handle_failure e vcs tty
 
-(** STM interface {{{******************************************************* **)
+(** STM interface ******************************************************* **)
 
 let stop_worker n = Slaves.cancel_worker n
 
@@ -1945,9 +1944,8 @@ let edit_at id =
         VCS.restore vcs;
         VCS.print ();
         raise e
-(* }}} *)
 
-(** Old tty interface {{{*************************************************** **)
+(** Old tty interface *************************************************** **)
 
 let interp verb (_,e as lexpr) =
   let clas = classify_vernac e in
@@ -2070,6 +2068,4 @@ let show_script ?proof () =
     msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
   with Vcs_aux.Expired -> ()
 
-(* }}} *)
-
 (* vim:set foldmethod=marker: *)