Compatibilité ocamlweb pour cible doc

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

7 files changed, 31 insertions, 27 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 71127a92d..059b13c57 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Util
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4ff60578a..03ad950c7 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -64,7 +64,7 @@ val interp_casted_openconstr    :
 (* [interp_type_with_implicits] extends [interp_type] by allowing
    implicits arguments in the ``rel'' part of [env]; the extra
    argument associates a list of implicit positions to identifiers
-   declared in the rel_context of [env] *)
+   declared in the [rel_context] of [env] *)
 val interp_type_with_implicits : 
   evar_map -> env -> full_implicits_env -> constr_expr -> types
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index fb4b2a423..6741e1a0a 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -80,7 +80,7 @@ val build_coq_eq_data : coq_leibniz_eq_data delayed
 val build_coq_eqT_data : coq_leibniz_eq_data delayed
 val build_coq_idT_data : coq_leibniz_eq_data delayed
 
-val build_coq_eq : constr delayed (* = (build_coq_eq_data()).eq *)
+val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
 val build_coq_f_equal2 : constr delayed
 val build_coq_eqT : constr delayed
 val build_coq_sym_eqT : constr delayed
diff --git a/interp/genarg.mli b/interp/genarg.mli
index af02a9ebe..042520151 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Util
 open Names
@@ -19,9 +19,9 @@ open Term
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a and_short_name = 'a * identifier located option
 
-(* In globalize tactics, we need to keep the initial constr_expr to recompute*)
+(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
-(* The constr_expr field is None in TacDef though *)
+(* The [constr_expr] field is [None] in TacDef though *)
 type rawconstr_and_expr = rawconstr * constr_expr option
 
 type open_constr = Evd.evar_map * Term.constr
@@ -39,6 +39,7 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
 
 (* The route of a generic argument, from parsing to evaluation
 
+\begin{verbatim}
               parsing        in_raw                           out_raw
     char stream ----> rawtype ----> rawconstr generic_argument ---->
                                                                    |
@@ -46,16 +47,18 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
                                                                    V
                           type  <---- constr generic_argument  <----
                                   out                            in
+\end{verbatim}
 
 To distinguish between the uninterpreted (raw) and the interpreted
-worlds, we annotate the type generic_argument by a phantom argument
-which is either constr_expr or constr (actually we add also a second
-argument raw_tactic_expr and tactic, but this is only for technical
+worlds, we annotate the type [generic_argument] by a phantom argument
+which is either [constr_expr] or [constr] (actually we add also a second
+argument [raw_tactic_expr] and [tactic], but this is only for technical
 reasons, because these types are undefined at the type of compilation
-of Genarg).
+of [Genarg]).
 
 Transformation for each type :
-tag   f                          raw open type          cooked closed type
+\begin{verbatim}
+tag                            raw open type            cooked closed type
 
 BoolArgType                    bool                     bool
 IntArgType                     int                      int
@@ -76,6 +79,7 @@ List0ArgType of argument_type
 List1ArgType of argument_type
 OptArgType of argument_type
 ExtraArgType of string         '_a                      '_b
+\end{verbatim}
 *)
 
 type ('a,'co,'ta) abstract_argument_type
@@ -175,7 +179,7 @@ val wit_pair :
   ('b,'co,'ta) abstract_argument_type ->
       ('a * 'b,'co,'ta) abstract_argument_type
 
-(* 'a generic_argument = (Sigma t:type. t[constr/'a]) *)
+(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
 type ('a,'b) generic_argument
 
 val fold_list0 : 
@@ -255,7 +259,7 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
 
    with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
 
-   in_generic is not typable; we replace the second argument by an absurd
+   [in_generic] is not typable; we replace the second argument by an absurd
    type (with no introduction rule)
 *)
 type an_arg_of_this_type
diff --git a/interp/notation.mli b/interp/notation.mli
index e803d65e7..0e401acd6 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -30,7 +30,7 @@ open Ppextend
 type level = precedence * tolerability list
 type delimiters = string
 type scope
-type scopes (* = scope_name list*)
+type scopes (* = [scope_name list] *)
 
 val type_scope : scope_name
 val declare_scope : scope_name -> unit
@@ -52,7 +52,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
 
 (*s Declare and uses back and forth a numeral interpretation *)
 
-(* A numeral interpreter is the pair of an interpreter for _integer_
+(* A numeral interpreter is the pair of an interpreter for **integer**
    numbers in terms and an optional interpreter in pattern, if
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
@@ -69,12 +69,12 @@ type required_module = global_reference * string list
 val declare_numeral_interpreter : scope_name -> required_module ->
   num_interpreter -> num_uninterpreter -> unit
 
-(* Returns the term/cases_pattern bound to a numeral in a given scope context*)
+(* Return the [term]/[cases_pattern] bound to a numeral in a given scope context*)
 val interp_numeral : loc -> bigint -> scope_name list -> rawconstr
 val interp_numeral_as_pattern : loc -> bigint -> name -> scope_name list ->
   cases_pattern
 
-(* Returns the numeral bound to a term/cases_pattern; raises No_match if no *)
+(* Return the numeral bound to a [term]/[cases_pattern]; raise [No_match] if no *)
 (* such numeral *)
 val uninterp_numeral : rawconstr -> scope_name * bigint
 val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
@@ -92,11 +92,11 @@ val declare_notation_interpretation : notation -> scope_name option ->
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
-(* Returns the interpretation bound to a notation *)
+(* Return the interpretation bound to a notation *)
 val interp_notation : loc -> notation -> scope_name list -> 
       interpretation * ((dir_path * string) * scope_name option)
 
-(* Returns the possible notations for a given term *)
+(* Return the possible notations for a given term *)
 val uninterp_notations : rawconstr ->
       (interp_rule * interpretation * int option) list
 val uninterp_cases_pattern_notations : cases_pattern ->
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 68927dbad..bddd1eef2 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4cfa0a0da..51fcd9c07 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
@@ -24,12 +24,12 @@ open Mod_subst
 (* non global expressions such as existential variables also *)
 
 type aconstr =
-  (* Part common to rawconstr and cases_pattern *)
+  (* Part common to [rawconstr] and [cases_pattern] *)
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
   | AList of identifier * identifier * aconstr * aconstr * bool
-  (* Part only in rawconstr *)
+  (* Part only in [rawconstr] *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
@@ -60,7 +60,7 @@ type scope_name = string
 type interpretation = 
     (identifier * (scope_name option * scope_name list)) list * aconstr
 
-val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation ->
+val match_aconstr : rawconstr -> interpretation ->
       (rawconstr * (scope_name option * scope_name list)) list
 
 (*s Concrete syntax for terms *)