From ec2948e7848265dbf547d97f0866ebd8f5cb6c97 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 20 Aug 2013 08:22:51 +0000
Subject: Declareops + Modops : more clever substitutions

 We try harder to preserve pointer equality when substituting.
 This will probably have little effect (for instance the
 constr_substituted are anyway _never_ substituted in place),
 but it cannot harm.

 Two particular cases:
 - we try to share (and maintain shared) mind_user_lc and mind_nf_lc
 - we try to share (and maintain shared) mod_expr and mod_type

 TODO: check that native compiler is still ok, since we might have
 less (ref NotLinked) now. Having references in constant_body and co
 is anyway a Very Bad Idea (TM).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.mli | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'kernel/modops.mli')

diff --git a/kernel/modops.mli b/kernel/modops.mli
index ea92c45ea..e148f9628 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -14,28 +14,33 @@ open Declarations
 open Entries
 open Mod_subst
 
-(** Various operations on modules and module types *)
+(** {6 Various operations on modules and module types } *)
 
+val module_body_of_type : module_path -> module_type_body  -> module_body
 
-val module_body_of_type : module_path -> module_type_body  -> module_body 
-
-val module_type_of_module : module_path option -> module_body ->
-  module_type_body
+val module_type_of_module :
+  module_path option -> module_body -> module_type_body
 
 val destr_functor :
   struct_expr_body -> MBId.t * module_type_body * struct_expr_body
 
+val check_modpath_equiv : env -> module_path -> module_path -> unit
+
+(** {6 Substitutions } *)
+
 val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
 
 val subst_signature : substitution -> structure_body -> structure_body
 
+(** {6 Adding to an environment } *)
+
 val add_signature :
   module_path -> structure_body -> delta_resolver -> env -> env
 
 (** adds a module and its components, but not the constraints *)
 val add_module : module_body -> env -> env
 
-val check_modpath_equiv : env -> module_path -> module_path -> unit
+(** {6 Strengthening } *)
 
 val strengthen : module_type_body -> module_path -> module_type_body
 
@@ -48,15 +53,19 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
 val subst_modtype_and_resolver : module_type_body -> module_path ->
   module_type_body
 
+(** {6 Cleaning a bound module expression } *)
+
 val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
 
+(** {6 Stm machinery : join and prune } *)
+
 val join_module_body : module_body -> unit
 val join_structure_body : structure_body -> unit
 val join_struct_expr_body : struct_expr_body -> unit
 
 val prune_structure_body : structure_body -> structure_body
 
-(** Errors *)
+(** {6 Errors } *)
 
 type signature_mismatch_error =
   | InductiveFieldExpected of mutual_inductive_body
@@ -78,7 +87,8 @@ type signature_mismatch_error =
   | NoTypeConstraintExpected
 
 type module_typing_error =
-  | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error
+  | SignatureMismatch of
+      Label.t * structure_field_body * signature_mismatch_error
   | LabelAlreadyDeclared of Label.t
   | ApplicationToNotPath of module_struct_entry
   | NotAFunctor of struct_expr_body
-- 
cgit v1.2.3