From 9b6517c0c933fb1d66c7feb53fa57e1697d8124a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 7 Jan 2010 15:32:49 +0000
Subject: Include can accept both Module and Module Type

 Syntax Include Type is still active, but deprecated, and triggers a warning.
 The syntax M <+ M' <+ M'', which performs internally an Include, also
 benefits from this: M, M', M'' can be independantly modules or module type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.ml  | 6 ++++++
 kernel/modops.mli | 4 ++++
 2 files changed, 10 insertions(+)

(limited to 'kernel')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 8c014c1d7d..000b2d65e6 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -61,6 +61,9 @@ let error_not_a_modtype_loc loc s =
 let error_not_a_module_loc loc s = 
   user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
 
+let error_not_a_module_or_modtype_loc loc s =
+  user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type."))
+
 let error_not_a_module s = error_not_a_module_loc dummy_loc s
 
 let error_not_a_constant l = 
@@ -86,6 +89,9 @@ let error_local_context lo =
 let error_no_such_label_sub l l1 =
   error ("The field "^(string_of_label l)^" is missing in "^l1^".")
 
+let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules."
+
+let error_application_to_module_type _ = error "Module application to a module type."
 
 let destr_functor env mtb =
   match mtb with
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 44d29ee3e4..435c196f9a 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -84,6 +84,8 @@ val error_not_a_modtype_loc : loc -> string -> 'a
 
 val error_not_a_module_loc : loc -> string -> 'a
 
+val error_not_a_module_or_modtype_loc : loc -> string -> 'a
+
 val error_not_a_module : string -> 'a
 
 val error_not_a_constant : label -> 'a
@@ -96,5 +98,7 @@ val error_local_context : label option -> 'a
 
 val error_no_such_label_sub : label->string->'a
 
+val error_with_in_module : unit -> 'a
 
+val error_application_to_module_type : unit -> 'a
 
-- 
cgit v1.2.3