From dc57718e98289b5d71a0a942d6a063d441dc6a54 Mon Sep 17 00:00:00 2001 From: soubiran Date: Wed, 24 Jan 2007 15:07:17 +0000 Subject: modifications des messages d'erreurs renvoyés lors de la comparaison de deux signatures de modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/modops.mli | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'kernel/modops.mli') diff --git a/kernel/modops.mli b/kernel/modops.mli index b8f1f66a3c..803bdc8398 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -17,7 +17,7 @@ open Declarations open Entries open Mod_subst (*i*) - +exception Circularity of string (* Various operations on modules and module types *) (* recursively unfold MTBdent module types *) @@ -98,5 +98,9 @@ val error_local_context : label option -> 'a val error_circular_with_module : identifier -> 'a +val error_circularity_in_subtyping : string->string->string-> 'a + +val error_no_such_label_sub : label->string->string->'a + val resolver_of_environment : mod_bound_id -> module_type_body -> module_path -> env -> resolver -- cgit v1.2.3