erreurs latex dans interfaces

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@287 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 12 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c28d35c8d..2b68faa0c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -63,20 +63,22 @@ val mis_consnames : mind_specif -> identifier array
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
 
-(* A light version of mind_specif_of_mind with pre-splitted args
+(* A light version of [mind_specif_of_mind] with pre-splitted args
    Invariant: We have
-   -- Hnf (fullmind) = DOPN(AppL,[|MutInd mind;..params..;..realargs..|])
-   -- with mind  = ((sp,i),localvars) for some sp, i, localvars
+
+   -- [Hnf (fullmind)] = [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])]
+
+   with [mind]  = [((sp,i),localvars)] for some [sp, i, localvars]
  *)
-type inductive_summary =
-    {fullmind : constr;
-     mind : inductive;
-     nparams : int;
-     nrealargs : int;
-     nconstr : int;
-     params : constr list;
-     realargs : constr list;
-     arity : constr}
+type inductive_summary = {
+  fullmind : constr;
+  mind : inductive;
+  nparams : int;
+  nrealargs : int;
+  nconstr : int;
+  params : constr list;
+  realargs : constr list;
+  arity : constr }
 
 (*s Declaration of inductive types. *)