From b1eef69751a05eebdbdc9d3091e1dae3386218d0 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 16 Aug 2002 10:00:36 +0000
Subject: 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
---
 kernel/modops.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/modops.mli')

diff --git a/kernel/modops.mli b/kernel/modops.mli
index 2401447852..7cd22c57c8 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
-- 
cgit v1.2.3