From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- kernel/conv_oracle.mli | 2 +- kernel/declarations.mli | 10 +++++----- kernel/environ.mli | 4 ++-- kernel/esubst.mli | 2 +- kernel/inductive.mli | 4 ++-- kernel/mod_typing.mli | 2 +- kernel/modops.mli | 4 ++-- 7 files changed, 14 insertions(+), 14 deletions(-) (limited to 'kernel') 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 -- cgit v1.2.3