Compatibilité ocamlweb pour cible doc

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

6 files changed, 12 insertions, 13 deletions

diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 3208bd593..2e8057cb0 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -36,7 +36,7 @@ type clausenv = {
   templval : constr freelisted;
   templtyp : constr freelisted }
 
-(* Substitution is not applied on templenv (because subst_clenv is
+(* Substitution is not applied on templenv (because [subst_clenv] is
    applied only on hints which typing env is overwritten by the
    goal env) *)
 val subst_clenv : substitution -> clausenv -> clausenv
@@ -47,7 +47,7 @@ val clenv_value     : clausenv -> constr
 val clenv_type      : clausenv -> types
 (* substitute resolved metas *)
 val clenv_nf_meta   : clausenv -> constr -> constr
-(* type of a meta in clenvś context *)
+(* type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
 val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
@@ -67,7 +67,7 @@ val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv
 (***************************************************************)
 (* Unification with clenvs *)
 
-(* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *)
+(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
 val clenv_unify : 
   bool -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
@@ -75,7 +75,7 @@ val clenv_unify :
 val clenv_unique_resolver :
   bool -> clausenv -> evar_info sigma -> clausenv
 
-(* same as above (allow_K=false) but replaces remaining metas
+(* same as above ([allow_K=false]) but replaces remaining metas
    with fresh evars *)
 val evar_clenv_unique_resolver :
   clausenv -> evar_info sigma -> clausenv
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 2bc813678..7f18a7943 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Names
 open Term
@@ -77,7 +77,7 @@ val make_arity_signature :
 val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
-(* Raise Not_found if not given an valid inductive type *)
+(* Raise [Not_found] if not given an valid inductive type *)
 val extract_mrectype : constr -> inductive * constr list
 val find_mrectype    : env -> evar_map -> constr -> inductive * constr list
 val find_rectype     : env -> evar_map -> constr -> inductive_type
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 2b0b8f240..b4f6c3245 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -40,7 +40,7 @@ val is_matching : constr_pattern -> constr -> bool
 val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 
 (* [match_subterm n pat c] returns the substitution and the context
-   corresponding to the [n+1]th _closed_ subterm of [c] matching [pat];
+   corresponding to the [n+1]th **closed** subterm of [c] matching [pat];
    It raises PatternMatchingFailure if no such matching exists *)
 val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 759e0adb6..b56e862ac 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -89,11 +89,11 @@ i*)
 
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
-(*
+(*i
 val map_rawconstr_with_binders_loc : loc -> 
   (identifier -> 'a -> identifier * 'a) ->
   ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
-*)
+i*)
 
 val occur_rawconstr : identifier -> rawconstr -> bool
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index b7d8c1b85..423a04723 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -65,7 +65,7 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
 (* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
-   [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *)
+   [t'=(x1:A1)..(xn:An)(ref args)] and raise [Not_found] if not possible *)
 val reduce_to_quantified_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index adc0e6daa..b290a5e5f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Util
 open Pp
@@ -16,7 +16,6 @@ open Sign
 open Environ
 
 (* Universes *)
-(*val set_module : Names.dir_path -> unit*)
 val new_univ : unit -> Univ.universe
 val new_sort_in_family : sorts_family -> sorts
 val new_Type : unit -> types
@@ -139,7 +138,7 @@ val named_hd_type : env -> types -> name -> name
 val mkProd_name : env -> name * types * types -> types
 val mkLambda_name : env -> name * types * constr -> constr
 
-(* Deprecated synonyms of mkProd_name and mkLambda_name *)
+(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
 val prod_name : env -> name * types * types -> types
 val lambda_name : env -> name * types * constr -> constr