diff options
| author | soubiran | 2007-01-24 15:07:17 +0000 |
|---|---|---|
| committer | soubiran | 2007-01-24 15:07:17 +0000 |
| commit | dc57718e98289b5d71a0a942d6a063d441dc6a54 (patch) | |
| tree | 3e8136faef19ef7d1e8280177de78c56582d1f35 /kernel/modops.mli | |
| parent | c155e42cdd1dd70b9e20243a6dc599ec653aef7a (diff) | |
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
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 6 |
1 files changed, 5 insertions, 1 deletions
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 |