Merge commit 'upstream/8.0pl2'

7 files changed, 14 insertions, 14 deletions

diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 77de9b8a..8d0c12bb 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: conv_oracle.mli,v 1.3.8.2 2004/07/16 19:30:24 herbelin Exp $ *)
+(*i $Id: conv_oracle.mli,v 1.3.8.3 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 open Names
 open Closure
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3252ddee..c670fe9a 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.mli,v 1.33.2.1 2004/07/16 19:30:24 herbelin Exp $ i*)
+(*i $Id: declarations.mli,v 1.33.2.2 2005/01/21 16:41:49 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -109,8 +109,8 @@ and module_specification_body =
     { msb_modtype : module_type_body;
       msb_equiv : module_path option; 
       msb_constraints : constraints }
-    (*    type_of(equiv) <: modtype  (if given)  
-       +  substyping of past With_Module mergers *)
+    (*    [type_of](equiv) <: modtype  (if given)  
+       +  substyping of past [With_Module] mergers *)
 
 
 type structure_elem_body = 
@@ -126,7 +126,7 @@ and module_expr_body =
   | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
   | MEBstruct of mod_self_id * module_structure_body
   | MEBapply of module_expr_body * module_expr_body  (* (F A) *)
-      * constraints  (* type_of(A) <: input_type_of(F) *)
+      * constraints  (* [type_of](A) <: [input_type_of](F) *)
 
 and module_body = 
     { mod_expr : module_expr_body option;
@@ -134,7 +134,7 @@ and module_body =
       mod_type : module_type_body;
       mod_equiv : module_path option;
       mod_constraints : constraints }
-    (*    type_of(mod_expr)  <: mod_user_type (if given)  *)
+    (*    [type_of(mod_expr)]  <: [mod_user_type] (if given)  *)
     (*  if equiv given then constraints are empty *)
 
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4e54761b..a2a66cb7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli,v 1.66.2.1 2004/07/16 19:30:25 herbelin Exp $ i*)
+(*i $Id: environ.mli,v 1.66.2.2 2005/01/21 16:41:49 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -44,7 +44,7 @@ val engagement    : env -> engagement option
 val empty_context : env -> bool
 
 (************************************************************************)
-(*s Context of de Bruijn variables (rel_context) *)
+(*s Context of de Bruijn variables ([rel_context]) *)
 val push_rel         : rel_declaration -> env -> env
 val push_rel_context :     rel_context -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index b02d747b..2fe981f7 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: esubst.mli,v 1.3.2.1 2004/07/16 19:30:25 herbelin Exp $ *)
+(*i $Id: esubst.mli,v 1.3.2.2 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 (*s Compact representation of explicit relocations. \\
    [ELSHFT(l,n)] == lift of [n], then apply [lift l].
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index ad44fa64..04345621 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli,v 1.57.8.1 2004/07/16 19:30:25 herbelin Exp $ i*)
+(*i $Id: inductive.mli,v 1.57.8.2 2005/01/21 16:41:49 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -62,7 +62,7 @@ val type_case_branches :
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
 
-(* Find the ultimate inductive in the mind_equiv chain *)
+(* Find the ultimate inductive in the [mind_equiv] chain *)
 
 val scrape_mind : env -> mutual_inductive -> mutual_inductive
 
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0ea98bf0..fdf39c56 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_typing.mli,v 1.2.8.1 2004/07/16 19:30:26 herbelin Exp $ *)
+(*i $Id: mod_typing.mli,v 1.2.8.2 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 (*i*)
 open Declarations
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 5433fa3e..cca2d315 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.mli,v 1.7.6.1 2004/07/16 19:30:26 herbelin Exp $ i*)
+(*i $Id: modops.mli,v 1.7.6.2 2005/01/21 16:41:50 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -41,7 +41,7 @@ val subst_signature_msid :
   module_signature_body -> module_signature_body
 
 (* [add_signature mp sign env] assumes that the substitution [msid]
-   \mapsto [mp] has already been performed (or is not necessary, like
+   $\mapsto$ [mp] has already been performed (or is not necessary, like
    when [mp = MPself msid]) *)
 val add_signature : 
   module_path -> module_signature_body -> env -> env