Some ocamldoc comments + Fixing name of .coqrc.version file in refman

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

4 files changed, 16 insertions, 12 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 824943d47..f808047b1 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -58,12 +58,14 @@ native-code versions of the system.
 \section[Resource file]{Resource file\index{Resource file}}
 
 When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
-resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is
-the home directory of the user.  If this file is not found, then the
-file \verb:$HOME/.coqrc: is searched. You can also specify an
-arbitrary name for the resource file (see option \verb:-init-file:
-below), or the name of another user to load the resource file of
-someone else (see option \verb:-user:).
+resource file \verb:$HOME/.coqrc.xxx: is loaded, where \verb:$HOME: is
+the home directory of the user and \verb:xxx: is the version number
+(e.g. 8.3).  If this file is not found, then the file
+\verb:$HOME/.coqrc: is searched. You can also specify an arbitrary
+name for the resource file (see option \verb:-init-file: below), or
+the name of another user to load the resource file of someone else
+(see option \verb:-user:).
+
 
 This file may contain, for instance, \verb:Add LoadPath: commands to add
 directories to the load path of \Coq.
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3e8de34c4..36af9dc48 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -40,7 +40,7 @@ type constant_body = {
     const_body : constr_substituted option;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-   (*i const_type_code : to_patch;i*)
+   (* const_type_code : to_patch;*)
     const_constraints : constraints;
     const_opaque : bool;
     const_inline : bool}
@@ -67,11 +67,11 @@ val recarg_length : wf_paths -> int -> int
 val subst_wf_paths : substitution -> wf_paths -> wf_paths
 
 (**
-{% \begin{verbatim} %}
+{v
    Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
    ...
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
-{% \end{verbatim} %}
+v}
 *)
 
 type monomorphic_inductive_arity = {
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 202b1aa4c..73bd2692e 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -89,8 +89,7 @@ val max_inductive_sort : sorts array -> universe
 val instantiate_universes : env -> rel_context ->
     polymorphic_arity -> types array -> rel_context * sorts
 
-(**************************************************************
-   Debug *)
+(** {6 Debug} *)
 
 type size = Large | Strict
 type subterm_spec =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 202a794ab..ab1f409ca 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -15,6 +15,9 @@ open Inductiveops
 open Rawterm
 open Evarutil
 
+(** {5 Compilation of pattern-matching } *)
+
+(** {6 Pattern-matching errors } *)
 type pattern_matching_error =
   | BadPattern of constructor * constr
   | BadConstructor of constructor * inductive
@@ -43,8 +46,8 @@ val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -
 val error_needs_inversion : env -> constr -> types -> 'a
 
 val set_impossible_default_clause : constr * types -> unit
-(** {6 Compilation of pattern-matching. } *)
 
+(** {6 Compilation primitive. } *)
 type alias_constr =
   | DepAlias
   | NonDepAlias