Strengthenning rules for modules + No modules in sections

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

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/modops.mli b/kernel/modops.mli
index 240144785..7cd22c57c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -51,6 +51,8 @@ val add_module :
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
+val strengthen : env -> module_type_body -> module_path -> module_type_body
+
 val error_existing_label : label -> 'a
 
 val error_declaration_not_path : module_expr -> 'a
@@ -62,6 +64,8 @@ val error_not_a_functor : module_expr -> 'a
 val error_incompatible_modtypes : 
   module_type_body -> module_type_body -> 'a
 
+val error_not_equal : module_path -> module_path -> 'a
+
 val error_not_match : label -> specification_body -> 'a
   
 val error_incompatible_labels : label -> label -> 'a