Fixing ml-doc.

2 files changed, 9 insertions, 9 deletions

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