summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2005-01-31 14:34:14 +0000
commite669490d0d5e6ed4bb45c895194791f01d038637 (patch)
tree4eb40b447e6573dbaa1cf593a2cae6758850cb7c /kernel
parentd334716fb2d09dd3304f98ee0dbf39275eac010b (diff)
parent6497f27021fec4e01f2182014f2bb1989b4707f9 (diff)
Merge commit 'upstream/8.0pl2'
Diffstat (limited to 'kernel')
-rw-r--r--kernel/conv_oracle.mli2
-rw-r--r--kernel/declarations.mli10
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/esubst.mli2
-rw-r--r--kernel/inductive.mli4
-rw-r--r--kernel/mod_typing.mli2
-rw-r--r--kernel/modops.mli4
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